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 Element of 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 Element of 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 13;
A6: A1 . (k + 1) in rng A1 by NAT_1:52;

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:52, 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 Element of NAT holds (Partial_Union A1) . n = {} ; :: thesis:

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

let x be set ; :: thesis:
assume x in Union (Partial_Union A1) ; :: thesis:
then ex n being Element of NAT st x in (Partial_Union A1) . n by PROB_1:25;
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 Element of NAT holds (Partial_Union A1) . n = {} ; :: thesis:

then consider n being Element of NAT such that
A10: (Partial_Union A1) . n <> {} ;
(Partial_Union A1) . n = Omega by A3, A10;
then for x being set st x in Omega holds
x in Union (Partial_Union A1) by PROB_1:25;
then 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:

end;

end;

end;

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

end;

A11: 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:10, PROB_1:11;
then for x being set st x in {{} ,Omega} holds
x in sigma X by TARSKI:def 2;
then A12: {{} ,Omega} c= sigma X by TARSKI:def 3;
assume X = {} ; :: thesis:
then A13: X c= {{} ,Omega} by XBOOLE_1:2;
for x being set st x in {{} ,Omega} holds
x in bool Omega

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

end;

then {{} ,Omega} is SigmaField of Omega by A1, A11, PROB_4:5, TARSKI:def 3;
then sigma X c= {{} ,Omega} by A13, PROB_1:def 14;
hence sigma X = {{} ,Omega} by A12, XBOOLE_0:def 10; :: thesis: