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))