defpred S₁[ set ] means $1 is Ordinal;
given X being set such that A1: for A being Ordinal holds A in X ; :: thesis: contradiction
consider Y being set such that
A2: for a being set holds
( a in Y iff ( a in X & S₁[a] ) ) from XBOOLE_0:sch 1();

now

let x be set ; :: thesis: ( x is Ordinal implies x in Y )
assume A3: x is Ordinal ; :: thesis: x in Y
then x in X by A1;
hence x in Y by A2, A3; :: thesis: verum

end;

then for x being set holds
( x in Y iff x is Ordinal ) by A2;
hence contradiction by Th37; :: thesis: verum