let X be set ; :: thesis: ( ( for x being object st x in X holds
x is Ordinal ) implies meet X is Ordinal )
assume A1: for x being object st x in X holds
x is Ordinal ; :: thesis: meet X is Ordinal

now :: thesis: ( X <> 0 implies meet X is Ordinal )

defpred S₁[ Ordinal] means $1 in X;
set x = the Element of X;
assume A2: X <> 0 ; :: thesis: meet X is Ordinal
then the Element of X is Ordinal by A1;
then A3: ex A being Ordinal st S₁[A] by A2;
consider A being Ordinal such that
A4: ( S₁[A] & ( for B being Ordinal st S₁[B] holds
A c= B ) ) from ORDINAL1:sch 1(A3);
for x being object holds
( x in A iff for Y being set st Y in X holds
x in Y )

proof

let x be object ; :: thesis: ( x in A iff for Y being set st Y in X holds
x in Y )
thus ( x in A implies for Y being set st Y in X holds
x in Y ) :: thesis: ( ( for Y being set st Y in X holds
x in Y ) implies x in A )

proof

assume A5: x in A ; :: 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 A6: Y in X ; :: thesis: x in Y
then reconsider B = Y as Ordinal by A1;
A c= B by A4, A6;
hence x in Y by A5; :: thesis: verum

end;

assume for Y being set st Y in X holds
x in Y ; :: thesis: x in A
hence x in A by A4; :: thesis: verum

end;

hence meet X is Ordinal by A2, SETFAM_1:def 1; :: thesis: verum

end;

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