let R1, R2 be LATTICE; ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & R1 is complete implies R2 is complete )
assume that
A1:
RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #)
and
A2:
R1 is complete
; R2 is complete
let X be set ; LATTICE3:def 12 ex b1 being Element of the carrier of R2 st
( X is_<=_than b1 & ( for b2 being Element of the carrier of R2 holds
( not X is_<=_than b2 or b1 <= b2 ) ) )
consider a1 being Element of R1 such that
A3:
X is_<=_than a1
and
A4:
for b being Element of R1 st X is_<=_than b holds
a1 <= b
by A2;
reconsider a2 = a1 as Element of R2 by A1;
take
a2
; ( X is_<=_than a2 & ( for b1 being Element of the carrier of R2 holds
( not X is_<=_than b1 or a2 <= b1 ) ) )
thus
X is_<=_than a2
by A1, A3, Lm10; for b1 being Element of the carrier of R2 holds
( not X is_<=_than b1 or a2 <= b1 )
let b2 be Element of R2; ( not X is_<=_than b2 or a2 <= b2 )
reconsider b1 = b2 as Element of R1 by A1;
assume
X is_<=_than b2
; a2 <= b2
then
X is_<=_than b1
by A1, Lm10;
hence
a2 <= b2
by A1, A4, Lm1; verum