let Omega be non empty set ; :: thesis: for Z being Field_Subset of Omega holds monotoneclass Z is Field_Subset of Omega
let Z be Field_Subset of Omega; :: thesis: monotoneclass Z is Field_Subset of Omega
A1: Z c= monotoneclass Z by Def15;
then reconsider Z1 = monotoneclass Z as non empty Subset-Family of Omega ;
A2: for y, Y being set st Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } holds
for z being set st z in Y holds
( z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in Z1 )

proof

let y, Y be set ; :: thesis: ( Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } implies for z being set st z in Y holds
( z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in Z1 ) )
assume A3: Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } ; :: thesis: for z being set st z in Y holds
( z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in Z1 )
thus for z being set st z in Y holds
( z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in Z1 ) :: thesis: verum

proof

let z be set ; :: thesis: ( z in Y implies ( z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in Z1 ) )
assume z in Y ; :: thesis: ( z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in Z1 )
then consider z1 being Element of Z1 such that
A4: ( z = z1 & y \ z1 in Z1 & z1 \ y in Z1 & z1 /\ y in Z1 ) by A3;
thus ( z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in Z1 ) by A4; :: thesis: verum

end;

end;

A5: for y being Element of Z1
for Y being set st Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } holds
Y is MonotoneClass of Omega

proof

let y be Element of Z1; :: thesis: for Y being set st Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } holds
Y is MonotoneClass of Omega
let Y be set ; :: thesis: ( Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } implies Y is MonotoneClass of Omega )
assume A6: Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } ; :: thesis: Y is MonotoneClass of Omega
A7: Y c= bool Omega

proof

for z being set st z in Y holds
z in Z1 by A2, A6;
then Y c= Z1 by TARSKI:def 3;
hence Y c= bool Omega by XBOOLE_1:1; :: thesis: verum

end;

( Y c= bool Omega & ( for A1 being SetSequence of Omega st A1 is monotone & rng A1 c= Y holds
lim A1 in Y ) )

proof

for A1 being SetSequence of Omega st A1 is monotone & rng A1 c= Y holds
lim A1 in Y

proof

let A1 be SetSequence of Omega; :: thesis: ( A1 is monotone & rng A1 c= Y implies lim A1 in Y )
assume that
A8: A1 is monotone and
A9: rng A1 c= Y ; :: thesis: lim A1 in Y
for n being Nat holds A1 . n in Z1

proof

let n be Nat; :: thesis: A1 . n in Z1
A1 . n in rng A1 by NAT_1:52;
then A1 . n in Y by A9;
hence A1 . n in Z1 by A2, A6; :: thesis: verum

end;

then B10: rng A1 c= Z1 by NAT_1:53;
A11: A1 is convergent by A8, SETLIM_1:65;
A12: A1 (\) y is monotone by A8, SETLIM_2:32;
for n being Nat holds (A1 (\) y) . n in Z1

proof

let n be Nat; :: thesis: (A1 (\) y) . n in Z1
A13: n in NAT by ORDINAL1:def 13;
A1 . n in rng A1 by NAT_1:52;
then A1 . n in Y by A9;
then (A1 . n) \ y in Z1 by A2, A6;
hence (A1 (\) y) . n in Z1 by A13, SETLIM_2:def 8; :: thesis: verum

end;

then rng (A1 (\) y) c= Z1 by NAT_1:53;
then A14: lim (A1 (\) y) in Z1 by A12, Th74;
A15: y (\) A1 is monotone by A8, SETLIM_2:29;
for n being Nat holds (y (\) A1) . n in Z1

proof

let n be Nat; :: thesis: (y (\) A1) . n in Z1
A16: n in NAT by ORDINAL1:def 13;
A1 . n in rng A1 by NAT_1:52;
then A1 . n in Y by A9;
then y \ (A1 . n) in Z1 by A2, A6;
hence (y (\) A1) . n in Z1 by A16, SETLIM_2:def 7; :: thesis: verum

end;

then rng (y (\) A1) c= Z1 by NAT_1:53;
then A17: lim (y (\) A1) in Z1 by A15, Th74;
A18: y (/\) A1 is monotone by A8, SETLIM_2:23;
for n being Nat holds (y (/\) A1) . n in Z1

proof

let n be Nat; :: thesis: (y (/\) A1) . n in Z1
A19: n in NAT by ORDINAL1:def 13;
A1 . n in rng A1 by NAT_1:52;
then A1 . n in Y by A9;
then y /\ (A1 . n) in Z1 by A2, A6;
hence (y (/\) A1) . n in Z1 by A19, SETLIM_2:def 5; :: thesis: verum

end;

then rng (y (/\) A1) c= Z1 by NAT_1:53;
then B: lim (y (/\) A1) in Z1 by A18, Th74;
B1: lim A1 is Element of Z1 by A8, Th74, B10;
( (lim A1) \ y in Z1 & y \ (lim A1) in Z1 & y /\ (lim A1) in Z1 ) by A11, A14, A17, SETLIM_2:92, SETLIM_2:94, SETLIM_2:95, B;
hence lim A1 in Y by A6, B1; :: thesis: verum

end;

hence ( Y c= bool Omega & ( for A1 being SetSequence of Omega st A1 is monotone & rng A1 c= Y holds
lim A1 in Y ) ) by A7; :: thesis: verum

end;

hence Y is MonotoneClass of Omega by Th74; :: thesis: verum

end;

A20: for y being Element of Z
for Y being set st Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } holds
Z1 c= Y

proof

let y be Element of Z; :: thesis: for Y being set st Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } holds
Z1 c= Y
let Y be set ; :: thesis: ( Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } implies Z1 c= Y )
assume A21: Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } ; :: thesis: Z1 c= Y
A22: Z c= Y

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in Z or z in Y )
assume A23: z in Z ; :: thesis: z in Y
then A24: z \ y in Z by PROB_1:12;
A25: y \ z in Z by A23, PROB_1:12;
z /\ y in Z by A23, FINSUB_1:def 2;
hence z in Y by A1, A21, A23, A24, A25; :: thesis: verum

end;

y in Z ;
then Y is MonotoneClass of Omega by A1, A5, A21;
hence Z1 c= Y by A22, Def15; :: thesis: verum

end;

A26: for y being Element of Z1
for Y being set st Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } holds
Z1 c= Y

proof

let y be Element of Z1; :: thesis: for Y being set st Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } holds
Z1 c= Y
let Y be set ; :: thesis: ( Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } implies Z1 c= Y )
assume A27: Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } ; :: thesis: Z1 c= Y
A28: Z c= Y

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in Z or z in Y )
assume A29: z in Z ; :: thesis: z in Y
set Y1 = { x where x is Element of Z1 : ( z \ x in Z1 & x \ z in Z1 & x /\ z in Z1 ) } ;
A30: Z1 c= { x where x is Element of Z1 : ( z \ x in Z1 & x \ z in Z1 & x /\ z in Z1 ) } by A20, A29;
y in Z1 ;
then ( z \ y in Z1 & y \ z in Z1 & z /\ y in Z1 ) by A2, A30;
hence z in Y by A1, A27, A29; :: thesis: verum

end;

Y is MonotoneClass of Omega by A5, A27;
hence Z1 c= Y by A28, Def15; :: thesis: verum

end;

A31: Z1 is cap-closed

proof

now

let y, z be set ; :: thesis: ( y in Z1 & z in Z1 implies y /\ z in Z1 )
assume A32: ( y in Z1 & z in Z1 ) ; :: thesis: y /\ z in Z1
set Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } ;
Z1 c= { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } by A26, A32;
hence y /\ z in Z1 by A2, A32; :: thesis: verum

end;

hence Z1 is cap-closed by FINSUB_1:def 2; :: thesis: verum

end;

for y being Subset of Omega st y in Z1 holds
y ` in Z1

proof

let y be Subset of Omega; :: thesis: ( y in Z1 implies y ` in Z1 )
assume A33: y in Z1 ; :: thesis: y ` in Z1
set Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } ;
Omega in Z by PROB_1:11;
then A34: Omega in Z1 by A1;
Z1 c= { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } by A26, A33;
then Omega \ y in Z1 by A2, A34;
hence y ` in Z1 by SUBSET_1:def 5; :: thesis: verum

end;

hence monotoneclass Z is Field_Subset of Omega by A31, PROB_1:def 1; :: thesis: verum