defpred S₁[ object ] means ex I being Ideal of X st $1 is I-congruence of X,I;
let A1, A2 be set ; :: thesis: ( ( for A1 being set holds
( A1 in A1 iff ex I being Ideal of X st A1 is I-congruence of X,I ) ) & ( for A1 being set holds
( A1 in A2 iff ex I being Ideal of X st A1 is I-congruence of X,I ) ) implies A1 = A2 )
assume that
A3: for x being set holds
( x in A1 iff ex I being Ideal of X st x is I-congruence of X,I ) and
A4: for x being set holds
( x in A2 iff ex I being Ideal of X st x is I-congruence of X,I ) ; :: thesis: A1 = A2
A5: for x being object holds
( x in A2 iff S₁[x] ) by A4;
A6: for x being object holds
( x in A1 iff S₁[x] ) by A3;
A1 = A2 from XBOOLE_0:sch 2(A6, A5);
hence A1 = A2 ; :: thesis: verum