theorem :: WAYBEL20:41

for L being complete continuous LATTICE
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) )