environ
vocabularies ENUMSET,RELATION,RELAT_AB;
notations ENUMSET,RELATION,RELAT_AB;
constructors ENUMSET,RELATION,RELAT_AB;
theorems ENUMSET,RELATION,RELAT_AB;
definitions ENUMSET,RELATION,RELAT_AB;

begin

reserve x,y,z,X,Y,Z for set;
reserve P,R,S for Relation;

::Zad1
X/\(Y\/Z) c= X/\Y\/X/\Z
proof
let x;
assume x in X/\(Y\/Z);
then x in X & x in Y\/Z by ENUMSET:def 7;
then x in X & (x in Y or x in Z) by ENUMSET:def 6;
then x in X & x in Y or x in X & x in Z by ENUMSET:def 7;
::>                                                    *602
then x in X/\Y or x in X/\Z by ENUMSET:def 7;
hence thesis by ENUMSET:def 6;
end;

::Zad2
X \ ( X \/ Y ) = {}
proof

  thus X \ ( X \/ Y ) c= {}
proof
let x;
assume x in  X \ ( X \/ Y );
then x in X & not x in X \/Y by ENUMSET:def 8;
then x in X & (not x in X & not x in Y) by ENUMSET:def 6;
hence thesis;
end;

thus {} c= X \ ( X \/ Y )
proof
let x;
assume x in {};
hence thesis by ENUMSET:def 1;
end;
end;

::Zad3
R"X \/ R"Y c= R" (X\/Y)
proof
let x;
assume x in R"X \/ R"Y;
then x in R"X or x in R"Y by ENUMSET:def 6;
then consider y such that A1:[x,y] in R & y in X or [x,y] in R & y in Y by RELAT_AB:def 4;
[x,y] in R & y in X\/Y by ENUMSET:def 6,A1;
hence thesis by RELAT_AB:def 4;
end;

::Zad4
ex A be set,P being Relation of A,A st P is weakly_connected & not P is connected
proof
set A={1,2};
set P={[1,2]};
reconsider P' = P as Relation by RELATION:1;

A1:dom P' c= A
proof
let x;
assume x in dom P';
then consider y such that A1:[x,y] in P' by RELAT_AB:def 1;
A2:[x,y] = [1,2] by A1,ENUMSET:def 3;
then A3:x = 1 & y = 2 by ENUMSET: 2;
thus x in A by A3,ENUMSET:def 4;
end;
A2:rng P' c= A
proof
let x;
assume x in rng P';
then consider y such that B1:[y,x] in P' by RELAT_AB:def 2;
B2:[y,x] = [1,2] by B1,ENUMSET:def 3;
then B3: y = 1 & x = 2 by ENUMSET: 2;
thus x in A by B3,ENUMSET:def 4;
end;

reconsider P''=P' as Relation of A,A by A1,A2,RELAT_AB:def 5;
take A,P'';

thus P'' is weakly_connected
proof
let x,y;
assume  x in A & y in A & x <> y;
then (x = 1 or x = 2) & (y = 1 or y = 2) & x <> y by ENUMSET:def 4;
then x = 1 & y = 2 or x = 2 & y = 1;
then [x,y] in P'' or x=2 & y = 1 by ENUMSET:def 3;
hence [x,y] in P'' or [y,x] in P'' by ENUMSET:def 3;
end;
thus not P'' is connected
proof
take x=1,y=1;
A1:x in A & y in A by ENUMSET:def 4;
not [1,1] in P''
proof
assume [1,1] in P'';
then [1,1] = [1,2] by ENUMSET:def 3;
hence contradiction by ENUMSET:2;
end;
then not [x,y] in P'' & not [y,x] in P'';
then A2:not ([x,y] in P'' or [y,x] in P'');
thus thesis by A1,A2;
end;
end;

::Zad5
ex P,R st dom (P/\R) <> dom P /\ dom R
proof
    reconsider P = {[1,1]}, R = {[1,2]} as Relation by RELATION:1;
    take P, R;
    T1: not 1 in dom (P /\ R)
    proof
      assume 1 in dom (P /\ R);
      then consider y such that A: [1, y] in P /\ R by RELAT_AB: def 1;
      [1, y] in P & [1, y] in R by A, ENUMSET: def 7;
      then [1, y] = [1, 1] & [1, y] = [1, 2] by ENUMSET: def 3;
      then y = 1 & y = 2 by ENUMSET: 2;
      then contradiction;
      hence thesis;
    end;
    S1: 1 in dom P
    proof
      [1, 1] in P by ENUMSET: def 3;
      hence thesis by RELAT_AB: def 1;
    end;
    S2: 1 in dom R
    proof
      [1, 2] in R by ENUMSET: def 3;
      hence thesis by RELAT_AB: def 1;
    end;
    1 in (dom P) /\ (dom R)
    proof
      S3: 1 in dom P by S1;
      S4: 1 in dom R by S2;
      hence thesis by S3, ENUMSET: def 7;
    end;    
    hence thesis by T1;

end;