let X be non empty set ; :: thesis: ( ( for a being set st a in X holds
a is cardinal number ) implies ex A being Cardinal st
( A in X & A = meet X ) )
assume A1: for a being set st a in X holds
a is cardinal number ; :: thesis: ex A being Cardinal st
( A in X & A = meet X )
defpred S₁[ Ordinal] means ( $1 in X & $1 is cardinal number );
A2: ex A being Ordinal st S₁[A]

proof

consider A being object such that
A3: A in X by XBOOLE_0:def 1;
reconsider A = A as Ordinal by A1, A3;
take A ; :: thesis: S₁[A]
thus S₁[A] by A1, A3; :: thesis: verum

end;

consider A being Ordinal such that
A4: ( S₁[A] & ( for B being Ordinal st S₁[B] holds
A c= B ) ) from ORDINAL1:sch 1(A2);
reconsider A = A as Cardinal by A4;
take A ; :: thesis: ( A in X & A = meet X )
thus A in X by A4; :: thesis: A = meet X
A5: meet X c= A by A4, SETFAM_1:3;

now :: thesis: for x being object st x in A holds
x in meet X

let x be object ; :: thesis: ( x in A implies x in meet X )
assume A6: x in A ; :: thesis: x in meet X

now :: thesis: for Y being set st Y in X holds
x in Y

let Y be set ; :: thesis: ( Y in X implies x in Y )
assume A7: Y in X ; :: thesis: x in Y
then reconsider B = Y as Ordinal by A1;
( B in X & B is cardinal number ) by A1, A7;
then A c= B by A4;
hence x in Y by A6; :: thesis: verum

end;

hence x in meet X by SETFAM_1:def 1; :: thesis: verum

end;

then A c= meet X by TARSKI:def 3;
hence A = meet X by A5, XBOOLE_0:def 10; :: thesis: verum