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 a9 = a as Element of R1 by A1;
assume D is_>=_than a ; :: thesis: a <= b
then D is_>=_than a9 by A1, Lm11;
then a9 <= "/\" (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