let P1, P2 be RelStr ; :: thesis: ( RelStr(# the carrier of P1, the InternalRel of P1 #) = RelStr(# the carrier of P2, the InternalRel of P2 #) implies for X being set
for a1 being Element of P1
for a2 being Element of P2 st a1 = a2 holds
( ( X is_<=_than a1 implies X is_<=_than a2 ) & ( X is_>=_than a1 implies X is_>=_than a2 ) ) )
assume A1: RelStr(# the carrier of P1, the InternalRel of P1 #) = RelStr(# the carrier of P2, the InternalRel of P2 #) ; :: thesis: for X being set
for a1 being Element of P1
for a2 being Element of P2 st a1 = a2 holds
( ( X is_<=_than a1 implies X is_<=_than a2 ) & ( X is_>=_than a1 implies X is_>=_than a2 ) )
let X be set ; :: thesis: for a1 being Element of P1
for a2 being Element of P2 st a1 = a2 holds
( ( X is_<=_than a1 implies X is_<=_than a2 ) & ( X is_>=_than a1 implies X is_>=_than a2 ) )
let a1 be Element of P1; :: thesis: for a2 being Element of P2 st a1 = a2 holds
( ( X is_<=_than a1 implies X is_<=_than a2 ) & ( X is_>=_than a1 implies X is_>=_than a2 ) )
let a2 be Element of P2; :: thesis: ( a1 = a2 implies ( ( X is_<=_than a1 implies X is_<=_than a2 ) & ( X is_>=_than a1 implies X is_>=_than a2 ) ) )
assume A2: a1 = a2 ; :: thesis: ( ( X is_<=_than a1 implies X is_<=_than a2 ) & ( X is_>=_than a1 implies X is_>=_than a2 ) )
thus ( X is_<=_than a1 implies X is_<=_than a2 ) :: thesis: ( X is_>=_than a1 implies X is_>=_than a2 )

proof

assume A3: for b being Element of P1 st b in X holds
b <= a1 ; :: according to LATTICE3:def 9 :: thesis: X is_<=_than a2
let b2 be Element of P2; :: according to LATTICE3:def 9 :: thesis: ( not b2 in X or b2 <= a2 )
assume b2 in X ; :: thesis: b2 <= a2
hence b2 <= a2 by A1, A2, A3, Th1; :: thesis: verum

end;

assume A4: for b being Element of P1 st b in X holds
a1 <= b ; :: according to LATTICE3:def 8 :: thesis: X is_>=_than a2
let b2 be Element of P2; :: according to LATTICE3:def 8 :: thesis: ( not b2 in X or a2 <= b2 )
assume b2 in X ; :: thesis: a2 <= b2
hence a2 <= b2 by A1, A2, A4, Th1; :: thesis: verum