let X be set ; :: thesis: for G being Subset-Family of X st G is upper holds
FinMeetCl G is upper
let G be Subset-Family of X; :: thesis: ( G is upper implies FinMeetCl G is upper )
assume A1: G is upper ; :: thesis: FinMeetCl G is upper

now :: thesis: for Y1, Y2 being Subset of X st Y1 in FinMeetCl G & Y1 c= Y2 holds
Y2 in FinMeetCl G

let Y1, Y2 be Subset of X; :: thesis: ( Y1 in FinMeetCl G & Y1 c= Y2 implies b₂ in FinMeetCl G )
assume that
A2: Y1 in FinMeetCl G and
A3: Y1 c= Y2 ; :: thesis: b₂ in FinMeetCl G
consider Z being Subset-Family of X such that
A4: Z c= G and
A5: Z is finite and
A6: Y1 = Intersect Z by A2, CANTOR_1:def 3;

per cases ( Z is empty or not Z is empty ) ;

suppose A7: Z is empty ; :: thesis: b₂ in FinMeetCl G

then Y2 = X by A6, A3, SETFAM_1:def 9;
hence Y2 in FinMeetCl G by A7, A6, SETFAM_1:def 9, A2; :: thesis: verum

end;

suppose A8: not Z is empty ; :: thesis: b₂ in FinMeetCl G

set Z2 = { (z \/ Y2) where z is Element of Z : verum } ;
set a = the Element of Z;
A9: the Element of Z \/ Y2 in { (z \/ Y2) where z is Element of Z : verum } ;
{ (z \/ Y2) where z is Element of Z : verum } c= bool X

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { (z \/ Y2) where z is Element of Z : verum } or t in bool X )
assume t in { (z \/ Y2) where z is Element of Z : verum } ; :: thesis: t in bool X
then consider u being Element of Z such that
A10: t = u \/ Y2 ;
A11: u in Z by A8;
u \/ Y2 c= X by XBOOLE_1:8, A11;
hence t in bool X by A10; :: thesis: verum

end;

then reconsider Z2 = { (z \/ Y2) where z is Element of Z : verum } as Subset-Family of X ;

now :: thesis: ( Z2 c= G & Z2 is finite & Y2 = Intersect Z2 )

now :: thesis: for x being object st x in Z2 holds
x in G

let x be object ; :: thesis: ( x in Z2 implies x in G )
assume A12: x in Z2 ; :: thesis: x in G
then reconsider y = x as Subset of X ;
consider u being Element of Z such that
A13: y = u \/ Y2 by A12;
u in G by A8, A4;
hence x in G by A13, XBOOLE_1:7, A1; :: thesis: verum

end;

hence Z2 c= G ; :: thesis: ( Z2 is finite & Y2 = Intersect Z2 )
A14: Z is finite by A5;
deffunc H₁( Element of Z) -> set = $1 \/ Y2;
A15: { H₁(z) where z is Element of Z : z in Z } is finite from FRAENKEL:sch 21(A14);

now :: thesis: ( { H₁(z) where z is Element of Z : z in Z } c= Z2 & Z2 c= { H₁(z) where z is Element of Z : z in Z } )

thus { H₁(z) where z is Element of Z : z in Z } c= Z2 :: thesis: Z2 c= { H₁(z) where z is Element of Z : z in Z }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H₁(z) where z is Element of Z : z in Z } or x in Z2 )
assume x in { H₁(z) where z is Element of Z : z in Z } ; :: thesis: x in Z2
then ex z being Element of Z st
( x = H₁(z) & z in Z ) ;
hence x in Z2 ; :: thesis: verum

end;

thus Z2 c= { H₁(z) where z is Element of Z : z in Z } :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Z2 or x in { H₁(z) where z is Element of Z : z in Z } )
assume x in Z2 ; :: thesis: x in { H₁(z) where z is Element of Z : z in Z }
then ex z being Element of Z st x = z \/ Y2 ;
hence x in { H₁(z) where z is Element of Z : z in Z } by A8; :: thesis: verum

end;

end;

hence Z2 is finite by A15; :: thesis: Y2 = Intersect Z2

now :: thesis: ( Y2 c= meet Z2 & meet Z2 c= Y2 )

thus Y2 c= meet Z2 :: thesis: meet Z2 c= Y2

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Y2 or x in meet Z2 )
assume A16: x in Y2 ; :: thesis: x in meet Z2

now :: thesis: for YY being set st YY in Z2 holds
x in YY

let YY be set ; :: thesis: ( YY in Z2 implies x in YY )
assume A17: YY in Z2 ; :: thesis: x in YY
then reconsider ZZ = YY as Subset of X ;
consider u being Element of Z such that
A18: ZZ = u \/ Y2 by A17;
Y2 c= u \/ Y2 by XBOOLE_1:7;
hence x in YY by A16, A18; :: thesis: verum

end;

hence x in meet Z2 by A9, SETFAM_1:def 1; :: thesis: verum

end;

thus meet Z2 c= Y2 :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet Z2 or x in Y2 )
assume A19: x in meet Z2 ; :: thesis: x in Y2
A20: for z being Element of Z holds x in z \/ Y2

proof

let z be Element of Z; :: thesis: x in z \/ Y2
z \/ Y2 in Z2 ;
hence x in z \/ Y2 by A19, SETFAM_1:def 1; :: thesis: verum

end;

for z being Element of Z holds
( x in z or x in Y2 )

proof

let z be Element of Z; :: thesis: ( x in z or x in Y2 )
x in z \/ Y2 by A20;
hence ( x in z or x in Y2 ) by XBOOLE_0:def 3; :: thesis: verum

end;

then ( for z being set st z in Z holds
x in z or x in Y2 ) ;
then ( x in meet Z or x in Y2 ) by A8, SETFAM_1:def 1;
then x in (meet Z) \/ Y2 by XBOOLE_0:def 3;
then A21: x in Y1 \/ Y2 by A8, A6, SETFAM_1:def 9;
Y1 \/ Y2 c= Y2 by A3, XBOOLE_1:8;
hence x in Y2 by A21; :: thesis: verum

end;

end;

hence Y2 = Intersect Z2 by A9, SETFAM_1:def 9; :: thesis: verum

end;

hence Y2 in FinMeetCl G by CANTOR_1:def 3; :: thesis: verum

end;

end;

end;

hence FinMeetCl G is upper ; :: thesis: verum