XBOOLE

theorem :: XBOOLE_1:1

for X, Y, Z being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) & Y : ( ( ) ( ) set ) c= Z : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) c= Z : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:3

for X being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= {} : ( ( ) ( empty ) set ) holds
X : ( ( ) ( ) set ) = {} : ( ( ) ( empty ) set ) ;

theorem :: XBOOLE_1:4

for X, Y, Z being ( ( ) ( ) set ) holds (X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \/ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) = X : ( ( ) ( ) set ) \/ (Y : ( ( ) ( ) set ) \/ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:5

for X, Y, Z being ( ( ) ( ) set ) holds (X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \/ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) = (X : ( ( ) ( ) set ) \/ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \/ (Y : ( ( ) ( ) set ) \/ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:6

for X, Y being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) \/ (X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:7

for X, Y being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:8

for X, Z, Y being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= Z : ( ( ) ( ) set ) & Y : ( ( ) ( ) set ) c= Z : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= Z : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:9

for X, Y, Z being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) \/ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) \/ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:10

for X, Y, Z being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) c= Z : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:11

for X, Y, Z being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= Z : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) c= Z : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:12

for X, Y being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) = Y : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:13

for X, Y, Z, V being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) & Z : ( ( ) ( ) set ) c= V : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) \/ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) \/ V : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:14

for Y, X, Z being ( ( ) ( ) set ) st Y : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) & Z : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) & ( for V being ( ( ) ( ) set ) st Y : ( ( ) ( ) set ) c= V : ( ( ) ( ) set ) & Z : ( ( ) ( ) set ) c= V : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) c= V : ( ( ) ( ) set ) ) holds
X : ( ( ) ( ) set ) = Y : ( ( ) ( ) set ) \/ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:15

for X, Y being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) = {} : ( ( ) ( empty ) set ) holds
X : ( ( ) ( ) set ) = {} : ( ( ) ( empty ) set ) ;

theorem :: XBOOLE_1:16

for X, Y, Z being ( ( ) ( ) set ) holds (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) /\ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) = X : ( ( ) ( ) set ) /\ (Y : ( ( ) ( ) set ) /\ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:17

for X, Y being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:18

for X, Y, Z being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) /\ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:19

for Z, X, Y being ( ( ) ( ) set ) st Z : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) & Z : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) holds
Z : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:20

for X, Y, Z being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) & X : ( ( ) ( ) set ) c= Z : ( ( ) ( ) set ) & ( for V being ( ( ) ( ) set ) st V : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) & V : ( ( ) ( ) set ) c= Z : ( ( ) ( ) set ) holds
V : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) ) holds
X : ( ( ) ( ) set ) = Y : ( ( ) ( ) set ) /\ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:21

for X, Y being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) /\ (X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = X : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:22

for X, Y being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) \/ (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = X : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:23

for X, Y, Z being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) /\ (Y : ( ( ) ( ) set ) \/ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \/ (X : ( ( ) ( ) set ) /\ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:24

for X, Y, Z being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) \/ (Y : ( ( ) ( ) set ) /\ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = (X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) /\ (X : ( ( ) ( ) set ) \/ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:25

for X, Y, Z being ( ( ) ( ) set ) holds ((X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \/ (Y : ( ( ) ( ) set ) /\ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \/ (Z : ( ( ) ( ) set ) /\ X : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = ((X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) /\ (Y : ( ( ) ( ) set ) \/ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) /\ (Z : ( ( ) ( ) set ) \/ X : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:26

for X, Y, Z being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) /\ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) /\ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:27

for X, Y, Z, V being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) & Z : ( ( ) ( ) set ) c= V : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) /\ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) /\ V : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:28

for X, Y being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) = X : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:29

for X, Y, Z being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) \/ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:30

for X, Z, Y being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= Z : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) \/ (Y : ( ( ) ( ) set ) /\ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = (X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) /\ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:31

for X, Y, Z being ( ( ) ( ) set ) holds (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \/ (X : ( ( ) ( ) set ) /\ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) \/ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:32

for X, Y being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) = Y : ( ( ) ( ) set ) \ X : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) = Y : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:33

for X, Y, Z being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) \ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) \ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:34

for X, Y, Z being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) holds
Z : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= Z : ( ( ) ( ) set ) \ X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:35

for X, Y, Z, V being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) & Z : ( ( ) ( ) set ) c= V : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) \ V : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) \ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:36

for X, Y being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:37

for X, Y being ( ( ) ( ) set ) holds
( X : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) = {} : ( ( ) ( empty ) set ) iff X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) ) ;

theorem :: XBOOLE_1:38

for X, Y being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) \ X : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) = {} : ( ( ) ( empty ) set ) ;

theorem :: XBOOLE_1:39

for X, Y being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) \/ (Y : ( ( ) ( ) set ) \ X : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:40

for X, Y being ( ( ) ( ) set ) holds (X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) = X : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:41

for X, Y, Z being ( ( ) ( ) set ) holds (X : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) = X : ( ( ) ( ) set ) \ (Y : ( ( ) ( ) set ) \/ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:42

for X, Y, Z being ( ( ) ( ) set ) holds (X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) = (X : ( ( ) ( ) set ) \ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \/ (Y : ( ( ) ( ) set ) \ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:43

for X, Y, Z being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) \/ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= Z : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:44

for X, Y, Z being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= Z : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) \/ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:45

for X, Y being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) holds
Y : ( ( ) ( ) set ) = X : ( ( ) ( ) set ) \/ (Y : ( ( ) ( ) set ) \ X : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:46

for X, Y being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) \ (X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = {} : ( ( ) ( empty ) set ) ;

theorem :: XBOOLE_1:47

for X, Y being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) \ (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = X : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:48

for X, Y being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) \ (X : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:49

for X, Y, Z being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) /\ (Y : ( ( ) ( ) set ) \ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:50

for X, Y, Z being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) /\ (Y : ( ( ) ( ) set ) \ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \ (X : ( ( ) ( ) set ) /\ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:51

for X, Y being ( ( ) ( ) set ) holds (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \/ (X : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = X : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:52

for X, Y, Z being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) \ (Y : ( ( ) ( ) set ) \ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = (X : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \/ (X : ( ( ) ( ) set ) /\ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:53

for X, Y, Z being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) \ (Y : ( ( ) ( ) set ) \/ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = (X : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) /\ (X : ( ( ) ( ) set ) \ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:54

for X, Y, Z being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) \ (Y : ( ( ) ( ) set ) /\ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = (X : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \/ (X : ( ( ) ( ) set ) \ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:55

for X, Y being ( ( ) ( ) set ) holds (X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \ (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = (X : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \/ (Y : ( ( ) ( ) set ) \ X : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:56

for X, Y, Z being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c< Y : ( ( ) ( ) set ) & Y : ( ( ) ( ) set ) c< Z : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) c< Z : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:57

for X, Y being ( ( ) ( ) set ) holds
( not X : ( ( ) ( ) set ) c< Y : ( ( ) ( ) set ) or not Y : ( ( ) ( ) set ) c< X : ( ( ) ( ) set ) ) ;

theorem :: XBOOLE_1:58

for X, Y, Z being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c< Y : ( ( ) ( ) set ) & Y : ( ( ) ( ) set ) c= Z : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) c< Z : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:59

for X, Y, Z being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) & Y : ( ( ) ( ) set ) c< Z : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) c< Z : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:60

for X, Y being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) holds
not Y : ( ( ) ( ) set ) c< X : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:61

for X being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) <> {} : ( ( ) ( empty ) set ) holds
{} : ( ( ) ( empty ) set ) c< X : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:62

for X being ( ( ) ( ) set ) holds not X : ( ( ) ( ) set ) c< {} : ( ( ) ( empty ) set ) ;

theorem :: XBOOLE_1:63

for X, Y, Z being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) & Y : ( ( ) ( ) set ) misses Z : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) misses Z : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:64

for A, X, B, Y being ( ( ) ( ) set ) st A : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) & B : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) & X : ( ( ) ( ) set ) misses Y : ( ( ) ( ) set ) holds
A : ( ( ) ( ) set ) misses B : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:65

for X being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) misses {} : ( ( ) ( empty ) set ) ;

theorem :: XBOOLE_1:66

for X being ( ( ) ( ) set ) holds
( X : ( ( ) ( ) set ) meets X : ( ( ) ( ) set ) iff X : ( ( ) ( ) set ) <> {} : ( ( ) ( empty ) set ) ) ;

theorem :: XBOOLE_1:67

for X, Y, Z being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) & X : ( ( ) ( ) set ) c= Z : ( ( ) ( ) set ) & Y : ( ( ) ( ) set ) misses Z : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) = {} : ( ( ) ( empty ) set ) ;

theorem :: XBOOLE_1:68

for Y, Z being ( ( ) ( ) set )
for A being ( ( non empty ) ( non empty ) set ) st A : ( ( non empty ) ( non empty ) set ) c= Y : ( ( ) ( ) set ) & A : ( ( non empty ) ( non empty ) set ) c= Z : ( ( ) ( ) set ) holds
Y : ( ( ) ( ) set ) meets Z : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:69

for Y being ( ( ) ( ) set )
for A being ( ( non empty ) ( non empty ) set ) st A : ( ( non empty ) ( non empty ) set ) c= Y : ( ( ) ( ) set ) holds
A : ( ( non empty ) ( non empty ) set ) meets Y : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:70

for X, Y, Z being ( ( ) ( ) set ) holds
( ( X : ( ( ) ( ) set ) meets Y : ( ( ) ( ) set ) or X : ( ( ) ( ) set ) meets Z : ( ( ) ( ) set ) ) iff X : ( ( ) ( ) set ) meets Y : ( ( ) ( ) set ) \/ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;

theorem :: XBOOLE_1:71

for X, Y, Z being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) = Z : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) & X : ( ( ) ( ) set ) misses Y : ( ( ) ( ) set ) & Z : ( ( ) ( ) set ) misses Y : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) = Z : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:72

for X9, Y9, X, Y being ( ( ) ( ) set ) st X9 : ( ( ) ( ) set ) \/ Y9 : ( ( ) ( ) set ) : ( ( ) ( ) set ) = X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) & X : ( ( ) ( ) set ) misses X9 : ( ( ) ( ) set ) & Y : ( ( ) ( ) set ) misses Y9 : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) = Y9 : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:73

for X, Y, Z being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) \/ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) & X : ( ( ) ( ) set ) misses Z : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:74

for X, Y, Z being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) meets Y : ( ( ) ( ) set ) /\ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) meets Y : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:75

for X, Y being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) meets Y : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) meets Y : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:76

for Y, Z, X being ( ( ) ( ) set ) st Y : ( ( ) ( ) set ) misses Z : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) misses X : ( ( ) ( ) set ) /\ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:77

for X, Y, Z being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) meets Y : ( ( ) ( ) set ) & X : ( ( ) ( ) set ) c= Z : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) meets Y : ( ( ) ( ) set ) /\ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:78

for X, Y, Z being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) misses Y : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) /\ (Y : ( ( ) ( ) set ) \/ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = X : ( ( ) ( ) set ) /\ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:79

for X, Y being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) misses Y : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:80

for X, Y, Z being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) misses Y : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) misses Y : ( ( ) ( ) set ) \ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:81

for X, Y, Z being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) misses Y : ( ( ) ( ) set ) \ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
Y : ( ( ) ( ) set ) misses X : ( ( ) ( ) set ) \ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:82

for X, Y being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) misses Y : ( ( ) ( ) set ) \ X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:83

for X, Y being ( ( ) ( ) set ) holds
( X : ( ( ) ( ) set ) misses Y : ( ( ) ( ) set ) iff X : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) = X : ( ( ) ( ) set ) ) ;

theorem :: XBOOLE_1:84

for X, Y, Z being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) meets Y : ( ( ) ( ) set ) & X : ( ( ) ( ) set ) misses Z : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) meets Y : ( ( ) ( ) set ) \ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:85

for X, Y, Z being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) misses Z : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:86

for X, Y, Z being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) & X : ( ( ) ( ) set ) misses Z : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) \ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:87

for Y, Z, X being ( ( ) ( ) set ) st Y : ( ( ) ( ) set ) misses Z : ( ( ) ( ) set ) holds
(X : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \/ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) = (X : ( ( ) ( ) set ) \/ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:88

for X, Y being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) misses Y : ( ( ) ( ) set ) holds
(X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) = X : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:89

for X, Y being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) misses X : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:90

for X, Y being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) \ (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) misses Y : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:91

for X, Y, Z being ( ( ) ( ) set ) holds (X : ( ( ) ( ) set ) \+\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \+\ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) = X : ( ( ) ( ) set ) \+\ (Y : ( ( ) ( ) set ) \+\ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:92

for X being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) \+\ X : ( ( ) ( ) set ) : ( ( ) ( ) set ) = {} : ( ( ) ( empty ) set ) ;

theorem :: XBOOLE_1:93

for X, Y being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) = (X : ( ( ) ( ) set ) \+\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \/ (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:94

for X, Y being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) = (X : ( ( ) ( ) set ) \+\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \+\ (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:95

for X, Y being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) = (X : ( ( ) ( ) set ) \+\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \+\ (X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:96

for X, Y being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) \+\ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:97

for X, Y, Z being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= Z : ( ( ) ( ) set ) & Y : ( ( ) ( ) set ) \ X : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= Z : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) \+\ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= Z : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:98

for X, Y being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) = X : ( ( ) ( ) set ) \+\ (Y : ( ( ) ( ) set ) \ X : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:99

for X, Y, Z being ( ( ) ( ) set ) holds (X : ( ( ) ( ) set ) \+\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) = (X : ( ( ) ( ) set ) \ (Y : ( ( ) ( ) set ) \/ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \/ (Y : ( ( ) ( ) set ) \ (X : ( ( ) ( ) set ) \/ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:100

for X, Y being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) = X : ( ( ) ( ) set ) \+\ (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:101

for X, Y being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) \+\ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) = (X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \ (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:102

for X, Y, Z being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) \ (Y : ( ( ) ( ) set ) \+\ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = (X : ( ( ) ( ) set ) \ (Y : ( ( ) ( ) set ) \/ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \/ ((X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) /\ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:103

for X, Y being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) misses X : ( ( ) ( ) set ) \+\ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:104

for X, Y being ( ( ) ( ) set ) holds
( ( X : ( ( ) ( ) set ) c< Y : ( ( ) ( ) set ) or X : ( ( ) ( ) set ) = Y : ( ( ) ( ) set ) or Y : ( ( ) ( ) set ) c< X : ( ( ) ( ) set ) ) iff X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) are_c=-comparable ) ;

theorem :: XBOOLE_1:105

for X, Y being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c< Y : ( ( ) ( ) set ) holds
Y : ( ( ) ( ) set ) \ X : ( ( ) ( ) set ) : ( ( ) ( ) set ) <> {} : ( ( ) ( empty ) set ) ;

theorem :: XBOOLE_1:106

for X, A, B being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= A : ( ( ) ( ) set ) \ B : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
( X : ( ( ) ( ) set ) c= A : ( ( ) ( ) set ) & X : ( ( ) ( ) set ) misses B : ( ( ) ( ) set ) ) ;

theorem :: XBOOLE_1:107

for X, A, B being ( ( ) ( ) set ) holds
( X : ( ( ) ( ) set ) c= A : ( ( ) ( ) set ) \+\ B : ( ( ) ( ) set ) : ( ( ) ( ) set ) iff ( X : ( ( ) ( ) set ) c= A : ( ( ) ( ) set ) \/ B : ( ( ) ( ) set ) : ( ( ) ( ) set ) & X : ( ( ) ( ) set ) misses A : ( ( ) ( ) set ) /\ B : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: XBOOLE_1:108

for X, A, Y being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= A : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= A : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:109

for X, A, Y being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= A : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= A : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:110

for X, A, Y being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= A : ( ( ) ( ) set ) & Y : ( ( ) ( ) set ) c= A : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) \+\ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= A : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:111

for X, Z, Y being ( ( ) ( ) set ) holds (X : ( ( ) ( ) set ) /\ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \ (Y : ( ( ) ( ) set ) /\ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = (X : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) /\ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:112

for X, Z, Y being ( ( ) ( ) set ) holds (X : ( ( ) ( ) set ) /\ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \+\ (Y : ( ( ) ( ) set ) /\ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = (X : ( ( ) ( ) set ) \+\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) /\ Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:113

for X, Y, Z, V being ( ( ) ( ) set ) holds ((X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \/ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \/ V : ( ( ) ( ) set ) : ( ( ) ( ) set ) = X : ( ( ) ( ) set ) \/ ((Y : ( ( ) ( ) set ) \/ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \/ V : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:114

for A, B, C, D being ( ( ) ( ) set ) st A : ( ( ) ( ) set ) misses D : ( ( ) ( ) set ) & B : ( ( ) ( ) set ) misses D : ( ( ) ( ) set ) & C : ( ( ) ( ) set ) misses D : ( ( ) ( ) set ) holds
(A : ( ( ) ( ) set ) \/ B : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \/ C : ( ( ) ( ) set ) : ( ( ) ( ) set ) misses D : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:115

for A being ( ( ) ( ) set ) holds not A : ( ( ) ( ) set ) c< {} : ( ( ) ( empty ) set ) ;

theorem :: XBOOLE_1:116

for X, Y, Z being ( ( ) ( ) set ) holds X : ( ( ) ( ) set ) /\ (Y : ( ( ) ( ) set ) /\ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) /\ (X : ( ( ) ( ) set ) /\ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: XBOOLE_1:117

for P, G, C being ( ( ) ( ) set ) st C : ( ( ) ( ) set ) c= G : ( ( ) ( ) set ) holds
P : ( ( ) ( ) set ) \ C : ( ( ) ( ) set ) : ( ( ) ( ) set ) = (P : ( ( ) ( ) set ) \ G : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \/ (P : ( ( ) ( ) set ) /\ (G : ( ( ) ( ) set ) \ C : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;