let R1, R2 be complete LATTICE; ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies for p, q being Element of R1 st p << q holds
for p9, q9 being Element of R2 st p = p9 & q = q9 holds
p9 << q9 )
assume A1:
RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #)
; for p, q being Element of R1 st p << q holds
for p9, q9 being Element of R2 st p = p9 & q = q9 holds
p9 << q9
let p, q be Element of R1; ( p << q implies for p9, q9 being Element of R2 st p = p9 & q = q9 holds
p9 << q9 )
assume A2:
p << q
; for p9, q9 being Element of R2 st p = p9 & q = q9 holds
p9 << q9
let p9, q9 be Element of R2; ( p = p9 & q = q9 implies p9 << q9 )
assume that
A3:
p = p9
and
A4:
q = q9
; p9 << q9
let D9 be non empty directed Subset of R2; WAYBEL_3:def 1 ( not q9 <= "\/" (D9,R2) or ex b1 being Element of the carrier of R2 st
( b1 in D9 & p9 <= b1 ) )
assume A5:
q9 <= sup D9
; ex b1 being Element of the carrier of R2 st
( b1 in D9 & p9 <= b1 )
reconsider D = D9 as non empty Subset of R1 by A1;
reconsider D = D as non empty directed Subset of R1 by A1, Lm14;
sup D = sup D9
by A1, Lm12;
then
q <= sup D
by A1, A4, A5, Lm1;
then consider d being Element of R1 such that
A6:
d in D
and
A7:
p <= d
by A2;
reconsider d9 = d as Element of R2 by A1;
take
d9
; ( d9 in D9 & p9 <= d9 )
thus
d9 in D9
by A6; p9 <= d9
thus
p9 <= d9
by A1, A3, A7, Lm1; verum