let P, Q be RelStr ; :: thesis: for p, q being Element of P
for p1, q1 being Element of Q st the InternalRel of P c= the InternalRel of Q & p = p1 & q = q1 & p <= q holds
p1 <= q1
let p, q be Element of P; :: thesis: for p1, q1 being Element of Q st the InternalRel of P c= the InternalRel of Q & p = p1 & q = q1 & p <= q holds
p1 <= q1
let p1, q1 be Element of Q; :: thesis: ( the InternalRel of P c= the InternalRel of Q & p = p1 & q = q1 & p <= q implies p1 <= q1 )
assume ( the InternalRel of P c= the InternalRel of Q & p = p1 & q = q1 & [p,q] in the InternalRel of P ) ; :: according to ORDERS_2:def 9 :: thesis: p1 <= q1
hence [p1,q1] in the InternalRel of Q ; :: according to ORDERS_2:def 9 :: thesis: verum