defpred S₁[ object ] means ( $1 in X & ex A being Ordinal st
( $1 = A & A is limit_ordinal ) );
let Y, Z be set ; :: thesis: ( ( for x being object holds
( x in Y iff ( x in X & ex A being Ordinal st
( x = A & A is limit_ordinal ) ) ) ) & ( for x being object holds
( x in Z iff ( x in X & ex A being Ordinal st
( x = A & A is limit_ordinal ) ) ) ) implies Y = Z )
assume that
A3: for x being object holds
( x in Y iff S₁[x] ) and
A4: for x being object holds
( x in Z iff S₁[x] ) ; :: thesis: Y = Z
thus Y = Z from XBOOLE_0:sch 2(A3, A4); :: thesis: verum