let R1, R2 be LATTICE; :: thesis: for X being set st RelStr(# the carrier of R1,the InternalRel of R1 #) = RelStr(# the carrier of R2,the InternalRel of R2 #) holds
for p1 being Element of R1
for p2 being Element of R2 st p1 = p2 & X is_>=_than p1 holds
X is_>=_than p2
let X be set ; :: thesis: ( RelStr(# the carrier of R1,the InternalRel of R1 #) = RelStr(# the carrier of R2,the InternalRel of R2 #) implies for p1 being Element of R1
for p2 being Element of R2 st p1 = p2 & X is_>=_than p1 holds
X is_>=_than p2 )
assume A1: RelStr(# the carrier of R1,the InternalRel of R1 #) = RelStr(# the carrier of R2,the InternalRel of R2 #) ; :: thesis: for p1 being Element of R1
for p2 being Element of R2 st p1 = p2 & X is_>=_than p1 holds
X is_>=_than p2
let p1 be Element of R1; :: thesis: for p2 being Element of R2 st p1 = p2 & X is_>=_than p1 holds
X is_>=_than p2
let p2 be Element of R2; :: thesis: ( p1 = p2 & X is_>=_than p1 implies X is_>=_than p2 )
assume that
A2: p1 = p2 and
A3: X is_>=_than p1 ; :: thesis: X is_>=_than p2
let b2 be Element of R2; :: according to LATTICE3:def 8 :: thesis: ( not b2 in X or p2 <= b2 )
reconsider b1 = b2 as Element of R1 by A1;
assume b2 in X ; :: thesis: p2 <= b2
then p1 <= b1 by A3, LATTICE3:def 8;
hence p2 <= b2 by A1, A2, Lm1; :: thesis: verum