let Omega be non empty set ; :: thesis: for X being Subset-Family of Omega st X = {} holds
sigma X = {{} ,Omega}
let X be Subset-Family of Omega; :: thesis: ( X = {} implies sigma X = {{} ,Omega} )
assume A0: X = {} ; :: thesis: sigma X = {{} ,Omega}
A1: {{} ,Omega} is SigmaField of Omega

proof

Y: for x being set st x in {{} ,Omega} holds
x in bool Omega

proof

let x be set ; :: thesis: ( x in {{} ,Omega} implies x in bool Omega )
assume x in {{} ,Omega} ; :: thesis: x in bool Omega
then ( x = {} or x = Omega ) by TARSKI:def 2;
then x c= Omega by XBOOLE_1:2;
hence x in bool Omega ; :: thesis: verum

end;

B1: for A1 being SetSequence of Omega st rng A1 c= {{} ,Omega} holds
Union A1 in {{} ,Omega}

proof

let A1 be SetSequence of Omega; :: thesis: ( rng A1 c= {{} ,Omega} implies Union A1 in {{} ,Omega} )
assume C0: rng A1 c= {{} ,Omega} ; :: thesis: Union A1 in {{} ,Omega}
C1: for n being Element of NAT holds
( (Partial_Union A1) . n = {} or (Partial_Union A1) . n = Omega )

proof

let n be Element of NAT ; :: thesis: ( (Partial_Union A1) . n = {} or (Partial_Union A1) . n = Omega )
defpred S₁[ Nat] means ( (Partial_Union A1) . $1 = {} or (Partial_Union A1) . $1 = Omega );
X: (Partial_Union A1) . 0 = A1 . 0 by PROB_3:def 2;
A1 . 0 in rng A1 by NAT_1:52;
then D0: S₁[ 0 ] by C0, X, TARSKI:def 2;
D1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume Z: ( (Partial_Union A1) . k = {} or (Partial_Union A1) . k = Omega ) ; :: thesis: S₁[k + 1]
reconsider k = k as Element of NAT by ORDINAL1:def 13;
X: A1 . (k + 1) in rng A1 by NAT_1:52;

per cases ( (Partial_Union A1) . (k + 1) = {} \/ (A1 . (k + 1)) or (Partial_Union A1) . (k + 1) = Omega \/ (A1 . (k + 1)) ) by Z, PROB_3:def 2;

suppose (Partial_Union A1) . (k + 1) = {} \/ (A1 . (k + 1)) ; :: thesis: S₁[k + 1]

hence S₁[k + 1] by C0, X, TARSKI:def 2; :: thesis: verum

end;

suppose F1: (Partial_Union A1) . (k + 1) = Omega \/ (A1 . (k + 1)) ; :: thesis: S₁[k + 1]

( A1 . (k + 1) = {} or A1 . (k + 1) = Omega ) by C0, X, TARSKI:def 2;
hence S₁[k + 1] by F1; :: thesis: verum

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(D0, D1);
hence ( (Partial_Union A1) . n = {} or (Partial_Union A1) . n = Omega ) ; :: thesis: verum

end;

( Union (Partial_Union A1) = {} or Union (Partial_Union A1) = Omega )

proof

per cases ( for n being Element of NAT holds (Partial_Union A1) . n = {} or ex n being Element of NAT st not (Partial_Union A1) . n = {} ) ;

suppose E0: for n being Element of NAT holds (Partial_Union A1) . n = {} ; :: thesis: ( Union (Partial_Union A1) = {} or Union (Partial_Union A1) = Omega )

for x being set holds not x in Union (Partial_Union A1)

proof

let x be set ; :: thesis: not x in Union (Partial_Union A1)
assume x in Union (Partial_Union A1) ; :: thesis: contradiction
then consider n being Element of NAT such that
G0: x in (Partial_Union A1) . n by PROB_1:25;
thus contradiction by G0, E0; :: thesis: verum

end;

hence ( Union (Partial_Union A1) = {} or Union (Partial_Union A1) = Omega ) by XBOOLE_0:def 1; :: thesis: verum

end;

suppose not for n being Element of NAT holds (Partial_Union A1) . n = {} ; :: thesis: ( Union (Partial_Union A1) = {} or Union (Partial_Union A1) = Omega )

then consider n being Element of NAT such that
F0: (Partial_Union A1) . n <> {} ;
(Partial_Union A1) . n = Omega by F0, C1;
then for x being set st x in Omega holds
x in Union (Partial_Union A1) by PROB_1:25;
then ( Union (Partial_Union A1) c= Omega & Omega c= Union (Partial_Union A1) ) by TARSKI:def 3;
hence ( Union (Partial_Union A1) = {} or Union (Partial_Union A1) = Omega ) by XBOOLE_0:def 10; :: thesis: verum

end;

end;

end;

then ( Union A1 = {} or Union A1 = Omega ) by PROB_3:17;
hence Union A1 in {{} ,Omega} by TARSKI:def 2; :: thesis: verum

end;

for A being Subset of Omega st A in {{} ,Omega} holds
A ` in {{} ,Omega}

proof

let A be Subset of Omega; :: thesis: ( A in {{} ,Omega} implies A ` in {{} ,Omega} )
assume A in {{} ,Omega} ; :: thesis: A ` in {{} ,Omega}
then ( A = {} or A = Omega ) by TARSKI:def 2;
then ( A ` = Omega or A ` = {} ) by XBOOLE_1:37;
hence A ` in {{} ,Omega} by TARSKI:def 2; :: thesis: verum

end;

hence {{} ,Omega} is SigmaField of Omega by Y, B1, PROB_4:5, TARSKI:def 3; :: thesis: verum

end;

X c= {{} ,Omega} by A0, XBOOLE_1:2;
then A2: sigma X c= {{} ,Omega} by A1, PROB_1:def 14;
( {} in sigma X & Omega in sigma X ) by PROB_1:42, PROB_1:43;
then for x being set st x in {{} ,Omega} holds
x in sigma X by TARSKI:def 2;
then {{} ,Omega} c= sigma X by TARSKI:def 3;
hence sigma X = {{} ,Omega} by A2, XBOOLE_0:def 10; :: thesis: verum