begin
theorem Th1:
for
X,
Y,
Z being
set st
X c= Y &
Y c= Z holds
X c= Z
theorem Th7:
for
X,
Y being
set holds
X c= X \/ Y
theorem Th8:
for
X,
Z,
Y being
set st
X c= Z &
Y c= Z holds
X \/ Y c= Z
theorem
for
X,
Y,
Z being
set st
X c= Y holds
X c= Z \/ Y
theorem
for
X,
Y,
Z being
set st
X \/ Y c= Z holds
X c= Z
theorem Th12:
for
X,
Y being
set st
X c= Y holds
X \/ Y = Y
theorem
for
X,
Y,
Z,
V being
set st
X c= Y &
Z c= V holds
X \/ Z c= Y \/ V
theorem
for
Y,
X,
Z being
set st
Y c= X &
Z c= X & ( for
V being
set st
Y c= V &
Z c= V holds
X c= V ) holds
X = Y \/ Z
theorem Th17:
for
X,
Y being
set holds
X /\ Y c= X
theorem
for
X,
Y,
Z being
set st
X c= Y /\ Z holds
X c= Y
theorem Th19:
for
Z,
X,
Y being
set st
Z c= X &
Z c= Y holds
Z c= X /\ Y
theorem
for
X,
Y,
Z being
set st
X c= Y &
X c= Z & ( for
V being
set st
V c= Y &
V c= Z holds
V c= X ) holds
X = Y /\ Z
theorem
for
X,
Y being
set holds
X /\ (X \/ Y) = X
theorem Th22:
for
X,
Y being
set holds
X \/ (X /\ Y) = X
theorem
for
X,
Y,
Z,
V being
set st
X c= Y &
Z c= V holds
X /\ Z c= Y /\ V
theorem Th28:
for
X,
Y being
set st
X c= Y holds
X /\ Y = X
Lm1:
for X, Y being set holds
( X \ Y = {} iff X c= Y )
theorem
for
X,
Y being
set st
X \ Y = Y \ X holds
X = Y
theorem Th33:
for
X,
Y,
Z being
set st
X c= Y holds
X \ Z c= Y \ Z
theorem Th34:
for
X,
Y,
Z being
set st
X c= Y holds
Z \ Y c= Z \ X
Lm2:
for X, Y, Z being set holds X \ (Y /\ Z) = (X \ Y) \/ (X \ Z)
theorem
for
X,
Y,
Z,
V being
set st
X c= Y &
Z c= V holds
X \ V c= Y \ Z
theorem Th36:
for
X,
Y being
set holds
X \ Y c= X
theorem
for
X,
Y being
set st
X c= Y \ X holds
X = {}
theorem Th39:
for
X,
Y being
set holds
X \/ (Y \ X) = X \/ Y
theorem
for
X,
Y being
set holds
(X \/ Y) \ Y = X \ Y
theorem Th41:
for
X,
Y,
Z being
set holds
(X \ Y) \ Z = X \ (Y \/ Z)
theorem Th42:
for
X,
Y,
Z being
set holds
(X \/ Y) \ Z = (X \ Z) \/ (Y \ Z)
theorem
for
X,
Y,
Z being
set st
X c= Y \/ Z holds
X \ Y c= Z
theorem
for
X,
Y,
Z being
set st
X \ Y c= Z holds
X c= Y \/ Z
theorem
for
X,
Y being
set st
X c= Y holds
Y = X \/ (Y \ X)
theorem Th47:
for
X,
Y being
set holds
X \ (X /\ Y) = X \ Y
theorem
for
X,
Y being
set holds
X \ (X \ Y) = X /\ Y
theorem Th49:
for
X,
Y,
Z being
set holds
X /\ (Y \ Z) = (X /\ Y) \ Z
theorem Th50:
for
X,
Y,
Z being
set holds
X /\ (Y \ Z) = (X /\ Y) \ (X /\ Z)
theorem Th51:
for
X,
Y being
set holds
(X /\ Y) \/ (X \ Y) = X
theorem Th52:
for
X,
Y,
Z being
set holds
X \ (Y \ Z) = (X \ Y) \/ (X /\ Z)
theorem
for
X,
Y,
Z being
set holds
X \ (Y \/ Z) = (X \ Y) /\ (X \ Z)
theorem Th55:
for
X,
Y being
set holds
(X \/ Y) \ (X /\ Y) = (X \ Y) \/ (Y \ X)
Lm3:
for X, Y, Z being set st X c= Y & Y c< Z holds
X c< Z
theorem
for
X,
Y,
Z being
set st
X c< Y &
Y c< Z holds
X c< Z
theorem
for
X,
Y being
set holds
( not
X c< Y or not
Y c< X ) ;
theorem
for
X,
Y,
Z being
set st
X c< Y &
Y c= Z holds
X c< Z
theorem
for
X,
Y,
Z being
set st
X c= Y &
Y c< Z holds
X c< Z by Lm3;
theorem Th60:
for
X,
Y being
set st
X c= Y holds
not
Y c< X
Lm4:
for X, Y being set holds X /\ Y misses X \+\ Y
Lm5:
for X, Y being set holds X \+\ Y = (X \/ Y) \ (X /\ Y)
begin
theorem
for
X,
A,
Y being
set st
X c= A holds
X /\ Y c= A
theorem Th109:
for
X,
A,
Y being
set st
X c= A holds
X \ Y c= A
theorem Th111:
for
X,
Z,
Y being
set holds
(X /\ Z) \ (Y /\ Z) = (X \ Y) /\ Z
theorem
for
P,
G,
C being
set st
C c= G holds
P \ C = (P \ G) \/ (P /\ (G \ C))