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_inf_of D,R2 by YELLOW_0:17;
A3: ex_inf_of D,R1 by YELLOW_0:17;
then D is_>=_than "/\" D,R1 by YELLOW_0:def 10;
then A4: D is_>=_than b by A1, Lm11;
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 a' = a as Element of R1 by A1;
assume D is_>=_than a ; :: thesis: a <= b
then D is_>=_than a' by A1, Lm11;
then a' <= "/\" D,R1 by A3, YELLOW_0:def 10;
hence a <= b by A1, Lm1; :: thesis: verum

end;

hence "/\" D,R1 = "/\" D,R2 by A2, A4, YELLOW_0:def 10; :: thesis: verum