let L be complete continuous LATTICE; :: thesis: for R being non empty Subset of [:L,L:] st R is CLCongruence holds
for x being set holds
( x is Element of (L ./. R) iff ex y being Element of L st x = Class (EqRel R),y )
let R be non empty Subset of [:L,L:]; :: thesis: ( R is CLCongruence implies for x being set holds
( x is Element of (L ./. R) iff ex y being Element of L st x = Class (EqRel R),y ) )
assume R is CLCongruence ; :: thesis: for x being set holds
( x is Element of (L ./. R) iff ex y being Element of L st x = Class (EqRel R),y )
then A1: the carrier of (L ./. R) = Class (EqRel R) by Def5;
let x be set ; :: thesis: ( x is Element of (L ./. R) iff ex y being Element of L st x = Class (EqRel R),y )

hereby :: thesis: ( ex y being Element of L st x = Class (EqRel R),y implies x is Element of (L ./. R) )

assume x is Element of (L ./. R) ; :: thesis: ex y being Element of L st x = Class (EqRel R),y
then x in Class (EqRel R) by A1;
then consider y being set such that
A2: y in the carrier of L and
A3: x = Class (EqRel R),y by EQREL_1:def 5;
reconsider y = y as Element of L by A2;
take y = y; :: thesis: x = Class (EqRel R),y
thus x = Class (EqRel R),y by A3; :: thesis: verum

end;

given y being Element of L such that A4: x = Class (EqRel R),y ; :: thesis: x is Element of (L ./. R)
thus x is Element of (L ./. R) by A1, A4, EQREL_1:def 5; :: thesis: verum