let P be pcs-Str ; :: thesis: for p, q being Element of
for p', q' being Element of st p = p' & q = q' holds
( p <= q iff q' <= p' )
let p, q be Element of ; :: thesis: for p', q' being Element of st p = p' & q = q' holds
( p <= q iff q' <= p' )
set R = pcs-reverse P;
let p', q' be Element of ; :: thesis: ( p = p' & q = q' implies ( p <= q iff q' <= p' ) )
assume that
A1: p = p' and
A2: q = q' ; :: thesis: ( p <= q iff q' <= p' )
A3: the InternalRel of (pcs-reverse P) = the InternalRel of P ~ by Def40;
thus ( p <= q implies q' <= p' ) :: thesis: ( q' <= p' implies p <= q )

proof

assume [p,q] in the InternalRel of P ; :: according to ORDERS_2:def 9 :: thesis: q' <= p'
hence [q',p'] in the InternalRel of (pcs-reverse P) by A1, A2, A3, RELAT_1:def 7; :: according to ORDERS_2:def 9 :: thesis: verum

end;

assume [q',p'] in the InternalRel of (pcs-reverse P) ; :: according to ORDERS_2:def 9 :: thesis: p <= q
hence [p,q] in the InternalRel of P by A1, A2, A3, RELAT_1:def 7; :: according to ORDERS_2:def 9 :: thesis: verum