let X be set ; :: thesis: ( ( for a being set st a in X holds
a is cardinal number ) implies meet X is cardinal number )
assume A1: for a being set st a in X holds
a is cardinal number ; :: thesis: meet X is cardinal number

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

suppose X = {} ; :: thesis: meet X is cardinal number

hence meet X is cardinal number by SETFAM_1:def 1; :: thesis: verum

end;

suppose X <> {} ; :: thesis: meet X is cardinal number

then consider A being Cardinal such that
A2: ( A in X & A = meet X ) by A1, Th15;
thus meet X is cardinal number by A2; :: thesis: verum

end;

end;