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 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 #) ; :: thesis: 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; :: thesis: ( p << q implies for p9, q9 being Element of R2 st p = p9 & q = q9 holds
p9 << q9 )
assume A2: p << q ; :: thesis: for p9, q9 being Element of R2 st p = p9 & q = q9 holds
p9 << q9
let p9, q9 be Element of R2; :: thesis: ( p = p9 & q = q9 implies p9 << q9 )
assume that
A3: p = p9 and
A4: q = q9 ; :: thesis: p9 << q9
let D9 be non empty directed Subset of R2; :: according to WAYBEL_3:def 1 :: thesis: ( not q9 <= "\/" (D9,R2) or ex b₁ being Element of the carrier of R2 st
( b₁ in D9 & p9 <= b₁ ) )
assume A5: q9 <= sup D9 ; :: thesis: ex b₁ being Element of the carrier of R2 st
( b₁ in D9 & p9 <= b₁ )
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 ; :: thesis: ( d9 in D9 & p9 <= d9 )
thus d9 in D9 by A6; :: thesis: p9 <= d9
thus p9 <= d9 by A1, A3, A7, Lm1; :: thesis: verum