let X be set ; :: thesis: for SFX being Subset-Family of X holds
( ( SFX is cap-closed & X in SFX ) iff FinMeetCl SFX c= SFX )
let F be Subset-Family of X; :: thesis: ( ( F is cap-closed & X in F ) iff FinMeetCl F c= F )

hereby :: thesis: ( FinMeetCl F c= F implies ( F is cap-closed & X in F ) )

assume that
A1: F is cap-closed and
A2: X in F ; :: thesis: FinMeetCl F c= F

now :: thesis: for x being object st x in FinMeetCl F holds
x in F

let x be object ; :: thesis: ( x in FinMeetCl F implies x in F )
assume A3: x in FinMeetCl F ; :: thesis: x in F
then reconsider x1 = x as Subset of X ;
consider Y being Subset-Family of X such that
A4: Y c= F and
A5: Y is finite and
A6: x1 = Intersect Y by A3, CANTOR_1:def 3;
defpred S₁[ Nat] means for Y being Subset-Family of X
for x being Subset of X st Y c= F & card Y = $1 & x = Intersect Y holds
x in F;
A7: S₁[ 0 ]

proof

let Y be Subset-Family of X; :: thesis: for x being Subset of X st Y c= F & card Y = 0 & x = Intersect Y holds
x in F
let x be Subset of X; :: thesis: ( Y c= F & card Y = 0 & x = Intersect Y implies x in F )
assume that
Y c= F and
A8: card Y = 0 and
A9: x = Intersect Y ; :: thesis: x in F
A10: Y = {} by A8;
reconsider x0 = x as set ;
thus x in F by A9, A10, SETFAM_1:def 9, A2; :: thesis: verum

end;

A11: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A12: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for Y being Subset-Family of X
for x being Subset of X st Y c= F & card Y = k + 1 & x = Intersect Y holds
x in F

let Y be Subset-Family of X; :: thesis: for x being Subset of X st Y c= F & card Y = k + 1 & x = Intersect Y holds
b₃ in F
let x be Subset of X; :: thesis: ( Y c= F & card Y = k + 1 & x = Intersect Y implies b₂ in F )
assume that
A13: Y c= F and
A14: card Y = k + 1 and
A15: x = Intersect Y ; :: thesis: b₂ in F
Y is finite set by A14;
then consider x1 being Element of Y, C being Subset of Y such that
A16: Y = C \/ {x1} and
A17: card C = k by A14, PRE_CIRC:24;
A18: ( C c= F & card C = k ) by A13, A17;
F c= bool X ;
then C c= bool X by A13;
then reconsider C0 = C as Subset-Family of X ;

per cases ( C = {} or C <> {} ) ;

suppose A19: C = {} ; :: thesis: b₂ in F

meet {x1} = x1 by SETFAM_1:10;
then x = x1 by A15, A16, A19, SETFAM_1:def 9;
hence x in F by A13, A16; :: thesis: verum

end;

suppose A20: C <> {} ; :: thesis: b₂ in F

then meet (C \/ {x1}) = (meet C) /\ (meet {x1}) by SETFAM_1:9;
then A21: meet Y = (meet C) /\ x1 by A16, SETFAM_1:10;
meet Y = Intersect Y by A16, SETFAM_1:def 9;
then A22: Intersect Y = (Intersect C0) /\ x1 by A20, A21, SETFAM_1:def 9;
A23: Intersect C0 in F by A12, A18;
x1 in F by A13, A16;
hence x in F by A22, A15, A23, A1; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A24: for k being Nat holds S₁[k] from NAT_1:sch 2(A7, A11);
reconsider CY = card Y as Nat by A5;
S₁[CY] by A24;
hence x in F by A4, A6; :: thesis: verum

end;

hence FinMeetCl F c= F ; :: thesis: verum

end;

assume A25: FinMeetCl F c= F ; :: thesis: ( F is cap-closed & X in F )

now :: thesis: for A, B being set st A in F & B in F holds
A /\ B in F

let A, B be set ; :: thesis: ( A in F & B in F implies A /\ B in F )
assume A26: ( A in F & B in F ) ; :: thesis: A /\ B in F
then ( A in bool X & B in bool X ) ;
then {A,B} c= bool X by TARSKI:def 2;
then reconsider AB = {A,B} as finite Subset-Family of X ;
( AB c= F & AB is finite & meet AB = Intersect AB ) by A26, TARSKI:def 2, SETFAM_1:def 9;
then meet AB in FinMeetCl F by CANTOR_1:def 3;
then A /\ B in FinMeetCl F by SETFAM_1:11;
hence A /\ B in F by A25; :: thesis: verum

end;

hence ( F is cap-closed & X in F ) by A25, CANTOR_1:8; :: thesis: verum