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 object such that
A2: y in the carrier of L and
A3: x = Class ((EqRel R),y) by EQREL_1:def 3;
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 3; :: thesis: verum