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;