let R, S be RelStr ; 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; 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; ( 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 A1:
( p = p9 & q = q9 & RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of S, the InternalRel of S #) )
; ( not p <= q or p9 <= q9 )
assume
p <= q
; p9 <= q9
then
[p9,q9] in the InternalRel of S
by A1, ORDERS_2:def 5;
hence
p9 <= q9
by ORDERS_2:def 5; verum