let R1, R2 be complete LATTICE; :: thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies for D being set holds "\/" (D,R1) = "\/" (D,R2) )
assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; :: thesis: for D being set holds "\/" (D,R1) = "\/" (D,R2)
let D be set ; :: thesis: "\/" (D,R1) = "\/" (D,R2)
reconsider b = "\/" (D,R1) as Element of R2 by A1;
A2: ex_sup_of D,R2 by YELLOW_0:17;
A3: ex_sup_of D,R1 by YELLOW_0:17;
then D is_<=_than "\/" (D,R1) by YELLOW_0:def 9;
then A4: D is_<=_than b by A1, Lm10;
for a being Element of R2 st D is_<=_than a holds
a >= b
proof
let a be Element of R2; :: thesis: ( D is_<=_than a implies a >= b )
reconsider a9 = a as Element of R1 by A1;
assume D is_<=_than a ; :: thesis: a >= b
then D is_<=_than a9 by A1, Lm10;
then a9 >= "\/" (D,R1) by A3, YELLOW_0:def 9;
hence a >= b by A1, Lm1; :: thesis: verum
end;
hence "\/" (D,R1) = "\/" (D,R2) by A2, A4, YELLOW_0:def 9; :: thesis: verum