:: deftheorem Def5 defines ./. WAYBEL20:def 5 :
for L being complete continuous LATTICE
for R being non empty Subset of [:L,L:] st R is CLCongruence holds
for b₃ being strict complete continuous LATTICE holds
( b₃ = L ./. R iff ( the carrier of b₃ = Class (EqRel R) & ( for x, y being Element of b₃ holds
( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) ) );