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 p', q' being Element of R2 st p = p' & q = q' holds
p' << q' )
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 p', q' being Element of R2 st p = p' & q = q' holds
p' << q'
let p, q be Element of R1; :: thesis: ( p << q implies for p', q' being Element of R2 st p = p' & q = q' holds
p' << q' )
assume A2: p << q ; :: thesis: for p', q' being Element of R2 st p = p' & q = q' holds
p' << q'
let p', q' be Element of R2; :: thesis: ( p = p' & q = q' implies p' << q' )
assume A3: ( p = p' & q = q' ) ; :: thesis: p' << q'
let D' be non empty directed Subset of R2; :: according to WAYBEL_3:def 1 :: thesis: ( not q' <= "\/" D',R2 or ex b₁ being Element of the carrier of R2 st
( b₁ in D' & p' <= b₁ ) )
assume A4: q' <= sup D' ; :: thesis: ex b₁ being Element of the carrier of R2 st
( b₁ in D' & p' <= b₁ )
reconsider D = D' as non empty Subset of R1 by A1;
reconsider D = D as non empty directed Subset of R1 by A1, Lm14;
sup D = sup D' by A1, Lm12;
then q <= sup D by A1, A3, A4, Lm1;
then consider d being Element of R1 such that
A5: ( d in D & p <= d ) by A2, WAYBEL_3:def 1;
reconsider d' = d as Element of R2 by A1;
take d' ; :: thesis: ( d' in D' & p' <= d' )
thus d' in D' by A5; :: thesis: p' <= d'
thus p' <= d' by A1, A3, A5, Lm1; :: thesis: verum