environ
vocabularies ENUMSET;
notations ENUMSET;
constructors ENUMSET;
definitions ENUMSET;
equalities ENUMSET;
theorems ENUMSET;
begin
reserve x,y,z,A,B,C for set;
::2.114
A \+\ B = B \+\ A
proof
thus A \+\ B c= B \+\ A
proof
let x;
assume x in A \+\ B;
then x in (A \ B) \/ (B \ A);:: by ENUMSET:def 9;
then x in (A \ B) or x in (B \ A) by ENUMSET:def 6;
:: then x in (B \ A) or x in (A \ B);
then x in (B \ A) \/ (A \ B) by ENUMSET:def 6;
hence x in B \+\ A;:: by ENUMSET:def 9;
end;
thus B \+\ A c= A \+\ B
proof
let x;
assume x in B \+\ A;
then x in (B \ A) \/ (A \ B);
then x in (B \ A) or x in (A \ B) by ENUMSET:def 6;
then x in (A \ B) \/ (B \ A) by ENUMSET:def 6;
hence x in A \+\ B;
end;
end;
l0:
A \/ B = B \/ A
proof
thus A \/ B c= B \/ A
proof
let x;
assume x in A \/ B;
then x in A or x in B by ENUMSET:def 6;
hence x in B \/ A by ENUMSET:def 6;
end;
let x;
assume x in B \/ A;
then x in B or x in A by ENUMSET:def 6;
hence x in A \/ B by ENUMSET:def 6;
end;
A \+\ B = B \+\ A
proof
A \+\ B = (B \ A) \/ (A \ B) by l0;
hence A \+\ B = B \+\ A;
end;
A \+\ B = B \+\ A by l0;
::2.119
l1:
A \+\ B = (A\/B) \ (A/\B)
proof
thus A \+\ B c= (A\/B) \ (A/\B)
proof
let x;
assume x in A \+\ B;
then x in (A \ B) or x in (B \ A) by ENUMSET:def 6;
then (x in A & not x in B) or (x in B & not x in A) by ENUMSET:def 8;
:: then (x in A or x in B) & not (x in A & x in B);
:: then x in A \/ B & not (x in A & x in B) by ENUMSET:def 6;
then x in A \/ B & not x in A /\ B by ENUMSET:def 7,def 6;
hence x in (A\/B) \ (A/\B) by ENUMSET:def 8;
end;
thus (A\/B) \ (A/\B) c= A \+\ B
proof
let y;
assume y in (A\/B) \ (A/\B);
then y in A \/ B & not y in A /\ B by ENUMSET:def 8;
:: then (y in A or y in B) & not y in A /\ B by ENUMSET:def 6;
then (y in A or y in B) & not (y in A & y in B) by ENUMSET:def 7,def 6;
:: then (y in A & not y in B) or (y in B & not y in A);
then y in A \ B or y in B \ A by ENUMSET:def 8;
hence y in A \+\ B by ENUMSET:def 6;
end;
end;
::2.120
A\/B = (A\+\B)\+\(A/\B)
proof
thus A\/B c= (A\+\B)\+\(A/\B)
proof
let x;
assume x in A\/B;
then per cases by ENUMSET:def 6;
suppose aa: x in A;
per cases;
suppose x in B;
then ab: x in A/\B by aa,ENUMSET:def 7;
then not x in (A\/B)\(A/\B) by ENUMSET:def 8;
then not x in (A\+\B) by l1;
then x in (A/\B)\(A\+\B) by ab,ENUMSET:def 8;
:: then x in (A\+\B)\(A/\B) or x in (A/\B)\(A\+\B);
then x in ((A\+\B)\(A/\B)) \/ ((A/\B)\(A\+\B)) by ENUMSET:def 6;
hence x in (A\+\B)\+\(A/\B) by ENUMSET:def 9;
end;
suppose na: not x in B;
then ab: not x in A /\ B by ENUMSET:def 7;
then x in A\B by aa,na,ENUMSET:def 8;
then x in (A\B) \/ (B\A) by ENUMSET:def 6;
then x in (A\+\B) by ENUMSET:def 9;
then x in (A\+\B) \ (A/\B) by ab,ENUMSET:def 8;
then x in ((A\+\B) \ (A/\B)) \/ ((A/\B)\(A\+\B)) by ENUMSET:def 6;
hence x in (A\+\B)\+\(A/\B);
end;
end;
suppose aa: x in B;
per cases;
suppose x in A;
then ab: x in A/\B by aa,ENUMSET:def 7;
then not x in (A\/B) \ (A/\B) by ENUMSET:def 8;
then not x in (A \+\ B) by l1;
then x in (A/\B) \ (A \+\ B) by ab,ENUMSET:def 8;
then x in ((A \+\ B) \ (A/\B)) \/ ((A/\B) \ (A \+\ B)) by ENUMSET:def 6;
hence x in (A \+\ B) \+\ (A/\B) by ENUMSET:def 9;
end;
suppose na: not x in A;
then ab: not x in A/\B by aa,ENUMSET:def 7;
x in B\A by aa,na,ENUMSET:def 8;
then x in (A\B) \/ (B\A) by ENUMSET:def 6;
then x in A \+\ B by ENUMSET:def 9;
then x in (A \+\ B) \ (A/\B) by ab,ENUMSET:def 8;
then x in ((A \+\ B) \ (A/\B)) \/ ((A/\B) \ (A \+\ B)) by ENUMSET:def 6;
hence x in (A \+\ B) \+\ (A/\B) by ENUMSET:def 9;
end;
end;
end;
thus (A\+\B)\+\(A/\B) c= A\/B
proof
let x;
assume x in (A\+\B)\+\(A/\B);
then x in (A\+\B) \ (A/\B) or x in (A/\B)\ (A\+\B) by ENUMSET:def 6;
then (x in A\+\B & not x in A/\B) or (x in A/\B & not x in A\+\B) by ENUMSET:def 8;
then per cases;
suppose x in A\+\B & not x in A/\B;
then x in (A\/B) \ (A/\B) & not x in A/\B by l1;
hence x in A\/B by ENUMSET:def 8;
end;
suppose x in A/\B & not x in A\+\B;
then x in A & x in B by ENUMSET:def 7;
hence x in A\/B by ENUMSET:def 6;
end;
end;
end;
::2.121
ex A,B,C st not A\/(B\+\C) = (A\/B)\+\(A\/C)
proof
take A={1};
take B={};
take C={1};
s: 1 in {1} by ENUMSET:def 3;
then j: 1 in A\/(B\+\C) by ENUMSET:def 6;
not 1 in (A\/B)\+\(A\/C)
proof
assume 1 in (A\/B)\+\(A\/C);
then 1 in ((A\/B)\/(A\/C)) \ ((A\/B)/\(A\/C)) by l1;
then spr: 1 in ((A\/B)\/(A\/C)) & not 1 in ((A\/B)/\(A\/C)) by ENUMSET:def 8;
then 1 in A\/B & 1 in A\/C by s,ENUMSET:def 6;
hence contradiction by spr,ENUMSET:def 7;
end;
then not A\/(B\+\C) c= (A\/B)\+\(A\/C) by j,ENUMSET:def 10;
hence not A\/(B\+\C) = (A\/B)\+\(A\/C) by ENUMSET:def 11;
end;