Theorem S.I.1If x and y are sets then {x,y} = {y,x} and {x,y} != O.ProofLet z = {x,y}. By Definition S.A.1 /\(a) (a:-z <=> (a = x or a = y)). Thus /\(a) (a:-z <=> (a = y or a = x)). So z = {y,x}. By Definition S.A.1 x:-{x,y}. Thus by Axiom ZF1 {x,y} != O.Definition S.I.2 - IntersectionLet x be a set. We define that n(x) = {a:-u(x)|/\(b:-x) a:-b}.Definition S.I.3 - Basic set operationsLet x,y be sets. We define that: x u y = u({x,y}), x n y = n({x,y}), x\y = {a:-x|!(a:-y)}. x u y, x n y and x\y are sets by Axiom ZF5 and Axiom ZF4.Theorem S.I.4If x,y,z are sets then the following statements are true. (1) x u y = z <=> /\(a) ( a:-z <=> (a:-x or a:-y) ), (2) x n y = z <=> /\(a) ( a:-z <=> (a:-x and a:-y) ), (3) x\y = z <=> /\(a) ( a:-z <=> a:-x and !(a:-y) ),Proof(1) Assume that x u y = z. By Definition S.I.3 z = u({x,y}). Take any set a. a:-z <=> a:-u({x,y}) <=> \/(w) w:-{x,y} and a:-w <=> \/(w) (w = x or w = y) and a:-w <=> a:-x or a:-y. We have showed (=>). Assume that /\(a) a:-z <=> (a:-x or a:-y). Take any set a. a:-z <=> (a:-x or a:-y) <=> \/(w) (w = x or w = y) and a:-w <=> \/(w) w:-{x,y} and a:-w <=> a:-u({x,y}) <=> a:-x u y. By Axiom ZF1 z = x u y. We have showed (<=). (2) Notice that: x n y = n({x,y}) = {a:-u({x,y}) | /\(b:-{x,y}) a:-b} = {a:-x u y | a:-x and a:-y}. Assume that x n y = z. Then z = {a:-x u y | a:-x and a:-y}. Take any set a. It is obvious that (a:-z => a:-x and a:-y). We have to show (a:-x and a:-y => a:-z). If a:-x and a:-y then by Definition S.A.1 and Definition S.I.3 a:-u({x,y}) = x u y. Thus by Definition S.A.2 a:-{b:-x u y | b:-x and b:-y}. So a:-z. We have showed that x n y = z => ( /\(a) a:-z <=> (a:-x and a:-y) ). Now, assume that /\(a) a:-z <=> a:-x and a:-y. Take any set a. a:-z <=> a:-x and a:-y <=> a:-{b:-x u y | b:-x and b:-y} <=> a:- x n y. By Axiom ZF1 z = x n y. We have showed that ( /\(a) a:-z <=> (a:-x and a:-y) ) => z = x n y. (3) x\y = z <=> z = {b:-x|!(b:-y)} <=> (a:-z <=> a:-x and !(a:-y)).Theorem S.I.5 - Bool AlgebraIf x,y,z are sets then the following statements are true. (1) x u O = x, (2) x u y = y u x, (3) (x u y) u z = x u (y u z), (4) x n O = O, (5) x n y = y n x, (6) (x n y) n z = x n (y n z), (7) x u (y n z) = (x u y) n (x u z), (8) x n (y u z) = (x n y) u (x n z), (9) z\(x u y) = (z\x) n (z\y), (10) z\(x n y) = (z\x) u (z\y).ProofOne can prove the statements above applying Theorem S.I.4 and Axiom ZF1.Definitin S.I.6 - InclusionLet x,y be sets. We define that x c y <=> ( /\(a) (a:-x => a:-y) ).Theorem S.I.7If x,y,z are sets then the following statements are true. (1) O c x, (2) x c x, (3) x c y and y c z => x c z, (4) x c y and y c x => x = y, (5) x c y => (z u x) c (z u y), (6) x c y => (z n x) c (z n y), (7) y\x c y.ProofOne can prove the statements above applying Theorem S.I.4 and Axiom ZF1.Theorem S.I.8If x,y,x are sets then the following statements are true. (1) x c y u x, (2) x c y n x. (3) y c x => x\(x\y) = y.Proof(1) By Theorem S.I.7.1 we have O c y. By Theorem S.I.7.5 and Theorem S.I.5.1 x = (O u x) c y u x. (2) By Theorem S.I.7.1 we have O c y. By Theorem S.I.7.5 and Theorem S.I.5.1 x = (O n x) c y n x. (3) We have x\(x\y) = {z:-x | !(z:-x\y)} = {z:-x | !(z:-x and !(x:-y))} = {z:-x | !(z:-x) or x:-y} = {z:-x | x:-y} = y.Theorem S.I.9If x,z are sets, z:-x and z != O then u(x) != O.ProofBy Definition S.A.1 /\(a) (a:-u(x) <=> \/(b:-x) a:-b). We have z:-x and z != O. Thus we have a:-z. Thus a:-u(x). So u(x) != O.