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 M = UniCl (FinMeetCl ((sigma M) \/ (omega M))) & lambda N = UniCl (FinMeetCl ((sigma N) \/ (omega N))) ) by WAYBEL19:33;
( sigma M = sigma N & omega M = omega N ) by A1, WAYBEL19:3, YELLOW_9:52;
hence lambda M = lambda N by A1, A2; :: thesis: verum