defpred S_{1}[ 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_{1}[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

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

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