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} )
A1: 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 A2: rng A1 c= {{},Omega} ; :: thesis: Union A1 in {{},Omega}
A3: for n being Nat holds
( (Partial_Union A1) . n = {} or (Partial_Union A1) . n = Omega )

proof

defpred S₁[ Nat] means ( (Partial_Union A1) . $1 = {} or (Partial_Union A1) . $1 = Omega );
let n be Nat; :: thesis: ( (Partial_Union A1) . n = {} or (Partial_Union A1) . n = Omega )
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

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

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

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

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

end;

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

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

end;

end;

end;

( (Partial_Union A1) . 0 = A1 . 0 & A1 . 0 in rng A1 ) by NAT_1:51, PROB_3:def 2;
then A8: S₁[ 0 ] by A2, TARSKI:def 2;
for k being Nat holds S₁[k] from NAT_1:sch 2(A8, A4);
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 Nat holds (Partial_Union A1) . n = {} or ex n being Nat st not (Partial_Union A1) . n = {} ) ;

suppose A9: for n being Nat holds (Partial_Union A1) . n = {} ; :: thesis: ( Union (Partial_Union A1) = {} or Union (Partial_Union A1) = Omega )

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

proof

given x being object such that A10: x in Union (Partial_Union A1) ; :: thesis: contradiction
reconsider x = x as set by TARSKI:1;
ex n being Nat st x in (Partial_Union A1) . n by PROB_1:12, A10;
hence contradiction by A9; :: 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 Nat holds (Partial_Union A1) . n = {} ; :: thesis: ( Union (Partial_Union A1) = {} or Union (Partial_Union A1) = Omega )

then consider n being Nat such that
A11: (Partial_Union A1) . n <> {} ;
(Partial_Union A1) . n = Omega by A3, A11;
then for x being object st x in Omega holds
x in Union (Partial_Union A1) by PROB_1:12;
then Omega c= Union (Partial_Union A1) ;
hence ( Union (Partial_Union A1) = {} or Union (Partial_Union A1) = Omega ) ; :: thesis: verum

end;

end;

end;

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

end;

A12: 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;

( {} in sigma X & Omega in sigma X ) by PROB_1:4, PROB_1:5;
then for x being object st x in {{},Omega} holds
x in sigma X by TARSKI:def 2;
then A13: {{},Omega} c= sigma X ;
assume X = {} ; :: thesis: sigma X = {{},Omega}
then A14: X c= {{},Omega} ;
for x being object st x in {{},Omega} holds
x in bool Omega

proof

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

end;

then {{},Omega} is SigmaField of Omega by A1, A12, PROB_4:4, TARSKI:def 3;
then sigma X c= {{},Omega} by A14, PROB_1:def 9;
hence sigma X = {{},Omega} by A13; :: thesis: verum