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 Def9;
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 ex z1 being Element of Z1 st
( z = z1 & y \ z1 in Z1 & z1 \ y in Z1 & z1 /\ y in Z1 ) by A3;
hence ( z in Z1 & y \ z in Z1 & z \ y in Z1 & z /\ y in Z1 ) ; :: thesis: verum

end;

end;

A4: 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 A5: 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
A6: 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
A7: A1 is monotone and
A8: rng A1 c= Y ; :: thesis: lim A1 in Y
A9: A1 is convergent by A7, SETLIM_1:65;
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:51;
hence A1 . n in Z1 by A2, A5, A8; :: thesis: verum

end;

then rng A1 c= Z1 by NAT_1:52;
then A10: lim A1 is Element of Z1 by A7, Th69;
for n being Nat holds (A1 (\) y) . n in Z1

proof

let n be Nat; :: thesis: (A1 (\) y) . n in Z1
A1 . n in rng A1 by NAT_1:51;
then ( n in NAT & (A1 . n) \ y in Z1 ) by A2, A5, A8, ORDINAL1:def 12;
hence (A1 (\) y) . n in Z1 by SETLIM_2:def 8; :: thesis: verum

end;

then A11: rng (A1 (\) y) c= Z1 by NAT_1:52;
for n being Nat holds (y (/\) A1) . n in Z1

proof

let n be Nat; :: thesis: (y (/\) A1) . n in Z1
A1 . n in rng A1 by NAT_1:51;
then ( n in NAT & y /\ (A1 . n) in Z1 ) by A2, A5, A8, ORDINAL1:def 12;
hence (y (/\) A1) . n in Z1 by SETLIM_2:def 5; :: thesis: verum

end;

then A12: rng (y (/\) A1) c= Z1 by NAT_1:52;
y (/\) A1 is monotone by A7, SETLIM_2:23;
then lim (y (/\) A1) in Z1 by A12, Th69;
then A13: y /\ (lim A1) in Z1 by A9, SETLIM_2:92;
for n being Nat holds (y (\) A1) . n in Z1

proof

let n be Nat; :: thesis: (y (\) A1) . n in Z1
A1 . n in rng A1 by NAT_1:51;
then ( n in NAT & y \ (A1 . n) in Z1 ) by A2, A5, A8, ORDINAL1:def 12;
hence (y (\) A1) . n in Z1 by SETLIM_2:def 7; :: thesis: verum

end;

then A14: rng (y (\) A1) c= Z1 by NAT_1:52;
y (\) A1 is monotone by A7, SETLIM_2:29;
then lim (y (\) A1) in Z1 by A14, Th69;
then A15: y \ (lim A1) in Z1 by A9, SETLIM_2:94;
A1 (\) y is monotone by A7, SETLIM_2:32;
then lim (A1 (\) y) in Z1 by A11, Th69;
then (lim A1) \ y in Z1 by A9, SETLIM_2:95;
hence lim A1 in Y by A5, A10, A15, A13; :: thesis: verum

end;

for z being object st z in Y holds
z in Z1 by A2, A5;
then Y c= Z1 ;
hence Y is MonotoneClass of Omega by A6, Th69, XBOOLE_1:1; :: thesis: verum

end;

A16: 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 A17: Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } ; :: thesis: Z1 c= Y
A18: Z c= Y

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Z or z in Y )
reconsider zz = z as set by TARSKI:1;
assume A19: z in Z ; :: thesis: z in Y
then A20: zz /\ y in Z by FINSUB_1:def 2;
( zz \ y in Z & y \ zz in Z ) by A19, PROB_1:6;
hence z in Y by A1, A17, A19, A20; :: thesis: verum

end;

y in Z ;
then Y is MonotoneClass of Omega by A1, A4, A17;
hence Z1 c= Y by A18, Def9; :: thesis: verum

end;

A21: 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 A22: Y = { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } ; :: thesis: Z1 c= Y
A23: Z c= Y

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Z or z in Y )
reconsider zz = z as set by TARSKI:1;
set Y1 = { x where x is Element of Z1 : ( zz \ x in Z1 & x \ zz in Z1 & x /\ zz in Z1 ) } ;
assume A24: z in Z ; :: thesis: z in Y
then A25: Z1 c= { x where x is Element of Z1 : ( zz \ x in Z1 & x \ zz in Z1 & x /\ zz in Z1 ) } by A16;
A26: y in Z1 ;
then A27: zz /\ y in Z1 by A2, A25;
( zz \ y in Z1 & y \ zz in Z1 ) by A2, A25, A26;
hence z in Y by A1, A22, A24, A27; :: thesis: verum

end;

Y is MonotoneClass of Omega by A4, A22;
hence Z1 c= Y by A23, Def9; :: thesis: verum

end;

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

proof

Omega in Z by PROB_1:5;
then A29: Omega in Z1 by A1;
let y be Subset of Omega; :: thesis: ( y in Z1 implies y ` in Z1 )
assume A30: 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 ) } ;
Z1 c= { x where x is Element of Z1 : ( y \ x in Z1 & x \ y in Z1 & x /\ y in Z1 ) } by A21, A30;
then Omega \ y in Z1 by A2, A29;
hence y ` in Z1 by SUBSET_1:def 4; :: thesis: verum

end;

now :: thesis: for y, z being set st y in Z1 & z in Z1 holds
y /\ z in Z1

let y, z be set ; :: thesis: ( y in Z1 & z in Z1 implies y /\ z in Z1 )
assume that
A31: y in Z1 and
A32: 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 A21, A31;
hence y /\ z in Z1 by A2, A32; :: thesis: verum

end;

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