let X be set ; :: thesis: for F being Subset-Family of X st F c= Fin X holds
meet F in Fin X
let F be Subset-Family of X; :: thesis: ( F c= Fin X implies meet F in Fin X )
assume A1: F c= Fin X ; :: thesis: meet F in Fin X

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

suppose F = {} ; :: thesis: meet F in Fin X

hence meet F in Fin X by FINSUB_1:7, SETFAM_1:1; :: thesis: verum

end;

suppose F <> {} ; :: thesis: meet F in Fin X

then consider A being object such that
A2: A in F by XBOOLE_0:def 1;
reconsider A = A as set by TARSKI:1;
meet F c= A by A2, SETFAM_1:3;
hence meet F in Fin X by A1, A2, Th1; :: thesis: verum

end;

end;