let X be set ; :: thesis:
let F be Subset-Family of X; :: thesis:

let x be object ; :: thesis:
assume A3: x in FinMeetCl F ; :: thesis:
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 ]

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

end;

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

let Y be Subset-Family of X; :: thesis:
let x be Subset of X; :: thesis:
assume that
A13: Y c= F and
A14: card Y = k + 1 and
A15: x = Intersect Y ; :: thesis:
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 ;

end;

end;

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

end;

end;

end;

end;