defpred S₁[ object ] means ex I being Ideal of X st $1 is I-congruence of X,I;
consider Y being set such that
A1: for x being object holds
( x in Y iff ( x in bool [: the carrier of X, the carrier of X:] & S₁[x] ) ) from XBOOLE_0:sch 1();
take Y ; :: thesis: for A1 being set holds
( A1 in Y iff ex I being Ideal of X st A1 is I-congruence of X,I )
let x be set ; :: thesis: ( x in Y iff ex I being Ideal of X st x is I-congruence of X,I )
thus ( x in Y implies ex I being Ideal of X st x is I-congruence of X,I ) by A1; :: thesis: ( ex I being Ideal of X st x is I-congruence of X,I implies x in Y )
given I being Ideal of X such that A2: x is I-congruence of X,I ; :: thesis: x in Y
thus x in Y by A1, A2; :: thesis: verum