environ
vocabularies ENUMSET;
notations ENUMSET;
constructors ENUMSET;
definitions ENUMSET;
equalities ENUMSET;
theorems ENUMSET;
begin
reserve a,x,y,z,A,B,C for set;
::2.68
for A,B holds A \/ B = B \/ A
proof
let A,B;
thus 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;
:: then x in B or x in A;
hence x in B \/ A by ENUMSET:def 6;
end;
thus B \/ A c= A \/ B
proof
let x;
assume x in B \/ A;
then x in B or x in A by ENUMSET:def 6;
:: then x in A or x in B;
hence x in A \/ B by ENUMSET:def 6;
end;
end;
end;
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;
::2.69
A /\ B = B /\ A
proof
thus A /\ B c= B /\ A
proof
let y;
assume y in A /\ B;
then y in A & y in B by ENUMSET:def 7;
hence y in B /\ A by ENUMSET:def 7;
end;
let y;
assume y in B /\ A;
then y in B & y in A by ENUMSET:def 7;
hence y in A /\ B by ENUMSET:def 7;
end;
::2.70
A /\ (B \/ C) = (A/\B) \/ (A/\C)
proof
thus A /\ (B \/ C) c= (A/\B) \/ (A/\C)
proof
let a;
assume a in A /\ (B \/ C);
then a in A & a in B\/C by ENUMSET:def 7;
then a in A & (a in B or a in C) by ENUMSET:def 6;
:: then (a in A & a in B) or (a in A & a in C);
then a in A /\ B or a in A /\ C by ENUMSET:def 7;
hence a in (A/\B) \/ (A/\C) by ENUMSET:def 6;
end;
thus (A/\B) \/ (A/\C) c= A /\ (B \/ C)
proof
let a;
assume a in (A/\B) \/ (A/\C);
then a in A/\B or a in A/\C by ENUMSET:def 6;
then (a in A & a in B) or (a in A & a in C) by ENUMSET:def 7;
:: then a in A & (a in B or a in C);
then a in A & a in B \/ C by ENUMSET:def 6;
hence a in A /\ (B \/ C) by ENUMSET:def 7;
end;
end;
::2.74
{} /\ A = {}
proof
thus {} /\ A c= {}
proof
let x;
assume x in {} /\ A;
:: then x in {} & x in A by ENUMSET:def 7;
:: then contradiction by ENUMSET:def 1;
hence x in {} by ENUMSET:def 7;
end;
thus {} c= {} /\ A
proof
let x;
assume x in {};
:: then contradiction by ENUMSET:def 1;
:: hence x in {} /\ A;
hence x in {} /\ A by ENUMSET:def 1;
end;
end;
::2.75
{} \/ A = A
proof
thus {} \/ A c= A
proof
let x;
assume x in {} \/ A;
then x in {} or x in A by ENUMSET:def 6;
hence x in A by ENUMSET:def 1;
end;
thus A c= {} \/ A
proof
let x;
assume x in A;
:: then x in {} or x in A;
hence x in {} \/ A by ENUMSET:def 6;
end;
end;
::2.81
(A\/B)\C = (A\C)\/(B\C)
proof
thus (A\/B)\C c= (A\C)\/(B\C)
proof
let x;
assume x in (A\/B)\C;
then x in A\/B & not x in C by ENUMSET:def 8;
then (x in A or x in B)& not x in C by ENUMSET:def 6;
:: then (x in A & not x in C) or (x in B & not x in C);
then x in A\C or x in B\C by ENUMSET:def 8;
hence x in (A\C)\/(B\C) by ENUMSET:def 6;
end;
thus (A\C)\/(B\C) c= (A\/B)\C
proof
let x;
assume x in (A\C)\/(B\C);
then x in A\C or x in B\C by ENUMSET:def 6;
then (x in A & not x in C) or (x in B & not x in C) by ENUMSET:def 8;
:: then (x in A or x in B) & not x in C;
then x in A\/B & not x in C by ENUMSET:def 6;
hence x in (A\/B)\C by ENUMSET:def 8;
end;
end;