let R, S be RelStr ; :: thesis: for p, q being Element of R
for p9, q9 being Element of S st p = p9 & q = q9 & RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of S, the InternalRel of S #) & p <= q holds
p9 <= q9
let p, q be Element of R; :: thesis: for p9, q9 being Element of S st p = p9 & q = q9 & RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of S, the InternalRel of S #) & p <= q holds
p9 <= q9
let p9, q9 be Element of S; :: thesis: ( p = p9 & q = q9 & RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of S, the InternalRel of S #) & p <= q implies p9 <= q9 )
assume that
A1: p = p9 and
A2: q = q9 and
A3: RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of S, the InternalRel of S #) ; :: thesis: ( not p <= q or p9 <= q9 )
assume p <= q ; :: thesis: p9 <= q9
then [p9,q9] in the InternalRel of S by A1, A2, A3, ORDERS_2:def 5;
hence p9 <= q9 by ORDERS_2:def 5; :: thesis: verum