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
( () . n = {} or () . n = Omega )
proof
defpred S1[ Nat] means ( () . \$1 = {} or () . \$1 = Omega );
let n be Nat; :: thesis: ( () . n = {} or () . n = Omega )
A4: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A5: ( (Partial_Union A1) . k = {} or () . k = Omega ) ; :: thesis: S1[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 ) . (k + 1) = {} \/ (A1 . (k + 1)) or () . (k + 1) = Omega \/ (A1 . (k + 1)) ) by ;
suppose (Partial_Union A1) . (k + 1) = {} \/ (A1 . (k + 1)) ; :: thesis: S1[k + 1]
hence S1[k + 1] by ; :: thesis: verum
end;
suppose A7: (Partial_Union A1) . (k + 1) = Omega \/ (A1 . (k + 1)) ; :: thesis: S1[k + 1]
( A1 . (k + 1) = {} or A1 . (k + 1) = Omega ) by ;
hence S1[k + 1] by A7; :: thesis: verum
end;
end;
end;
( (Partial_Union A1) . 0 = A1 . 0 & A1 . 0 in rng A1 ) by ;
then A8: S1[ 0 ] by ;
for k being Nat holds S1[k] from NAT_1:sch 2(A8, A4);
hence ( (Partial_Union A1) . n = {} or () . n = Omega ) ; :: thesis: verum
end;
( Union () = {} or Union () = Omega )
proof
per cases ( for n being Nat holds () . n = {} or ex n being Nat st not () . n = {} ) ;
suppose A9: for n being Nat holds () . n = {} ; :: thesis: ( Union () = {} or Union () = Omega )
for x being object holds not x in Union ()
proof
given x being object such that A10: x in Union () ; :: thesis: contradiction
reconsider x = x as set by TARSKI:1;
ex n being Nat st x in () . n by ;
hence contradiction by A9; :: thesis: verum
end;
hence ( Union () = {} or Union () = Omega ) by XBOOLE_0:def 1; :: thesis: verum
end;
suppose not for n being Nat holds () . n = {} ; :: thesis: ( Union () = {} or Union () = Omega )
then consider n being Nat such that
A11: (Partial_Union A1) . n <> {} ;
(Partial_Union A1) . n = Omega by ;
then for x being object st x in Omega holds
x in Union () by PROB_1:12;
then Omega c= Union () ;
hence ( Union () = {} or Union () = 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 ;
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 ;
then sigma X c= {{},Omega} by ;
hence sigma X = {{},Omega} by A13; :: thesis: verum