let P be pcs-Str ; :: thesis: for p, q being Element of P
for p9, q9 being Element of (pcs-reverse P) st p = p9 & q = q9 holds
( p <= q iff q9 <= p9 )
let p, q be Element of P; :: thesis: for p9, q9 being Element of (pcs-reverse P) st p = p9 & q = q9 holds
( p <= q iff q9 <= p9 )
set R = pcs-reverse P;
let p9, q9 be Element of (pcs-reverse P); :: thesis: ( p = p9 & q = q9 implies ( p <= q iff q9 <= p9 ) )
assume that
A1: p = p9 and
A2: q = q9 ; :: thesis: ( p <= q iff q9 <= p9 )
A3: the InternalRel of (pcs-reverse P) = the InternalRel of P ~ by Def40;
thus ( p <= q implies q9 <= p9 ) by A1, A2, A3, RELAT_1:def 7; :: thesis: ( q9 <= p9 implies p <= q )
assume [q9,p9] in the InternalRel of (pcs-reverse P) ; :: according to ORDERS_2:def 5 :: thesis: p <= q
hence [p,q] in the InternalRel of P by A1, A2, A3, RELAT_1:def 7; :: according to ORDERS_2:def 5 :: thesis: verum