let M, N be complete LATTICE; :: thesis: ( RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of N, the InternalRel of N #) implies lambda M = lambda N )
assume A1: RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of N, the InternalRel of N #) ; :: thesis: lambda M = lambda N
A2: lambda N = UniCl (FinMeetCl ((sigma N) \/ (omega N))) by WAYBEL19:33;
A3: lambda M = UniCl (FinMeetCl ((sigma M) \/ (omega M))) by WAYBEL19:33;
sigma M = sigma N by A1, YELLOW_9:52;
hence lambda M = lambda N by A1, A3, A2, WAYBEL19:3; :: thesis: verum