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