theorem :: WAYBEL30:11

for M, N being complete LATTICE st RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of N, the InternalRel of N #) holds
lambda M = lambda N