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 st p << q holds
for p', q' being Element of 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 st p << q holds
for p', q' being Element of st p = p' & q = q' holds
p' << q'
let p, q be Element of ; :: thesis: ( p << q implies for p', q' being Element of st p = p' & q = q' holds
p' << q' )
assume A2: p << q ; :: thesis: for p', q' being Element of st p = p' & q = q' holds
p' << q'
let p', q' be Element of ; :: thesis: ( p = p' & q = q' implies p' << q' )
assume that
A3: p = p' and
A4: q = q' ; :: thesis: p' << q'
let D' be non empty directed Subset of ; :: 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 A5: 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 by A1;
reconsider D = D as non empty directed Subset of by A1, Lm14;
sup D = sup D' by A1, Lm12;
then q <= sup D by A1, A4, A5, Lm1;
then consider d being Element of such that
A6: d in D and
A7: p <= d by A2, WAYBEL_3:def 1;
reconsider d' = d as Element of by A1;
take d' ; :: thesis: ( d' in D' & p' <= d' )
thus d' in D' by A6; :: thesis: p' <= d'
thus p' <= d' by A1, A3, A7, Lm1; :: thesis: verum