let Omega be non empty set ; :: thesis:
let X be Subset-Family of Omega; :: thesis:
A1: for A1 being SetSequence of Omega st rng A1 c= {{},Omega} holds
Union A1 in {{},Omega}

let A1 be SetSequence of Omega; :: thesis:
assume A2: rng A1 c= {{},Omega} ; :: thesis:
A3: for n being Nat holds
( (Partial_Union A1) . n = {} or (Partial_Union A1) . n = Omega )

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

let k be Nat; :: thesis:
assume A5: ( (Partial_Union A1) . k = {} or (Partial_Union A1) . k = Omega ) ; :: thesis:
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 (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:

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

end;

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

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

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:

end;

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

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

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

given x being object such that A10: x in Union (Partial_Union A1) ; :: thesis:
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:

end;

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

end;

suppose not for n being Nat holds (Partial_Union A1) . n = {} ; :: thesis:

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:

end;

end;

end;

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

end;

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

let A be Subset of Omega; :: thesis:
assume A in {{},Omega} ; :: thesis:
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:

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:
then A14: X c= {{},Omega} ;
for x being object st x in {{},Omega} holds
x in bool Omega

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

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: