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