defpred S₁[ object ] 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 object holds
( a in Y iff ( a in X & S₁[a] ) ) from XBOOLE_0:sch 1();
for x being set st x is Ordinal holds
x in Y by A1, A2;
then for x being set holds
( x in Y iff x is Ordinal ) by A2;
hence contradiction by Th21; :: thesis: verum