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 that
A1: p = p' and
A2: q = q' 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 p' <= q' )
assume p <= q ; :: thesis: p' <= q'
then [p',q'] in the InternalRel of S by A1, A2, A3, ORDERS_2:def 9;
hence p' <= q' by ORDERS_2:def 9; :: thesis: verum