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 that
A1: the InternalRel of P c= the InternalRel of Q and
A2: p = p1 and
A3: q = q1 and
A4: [p,q] in the InternalRel of P ; :: according to ORDERS_2:def 5 :: thesis: p1 <= q1
thus [p1,q1] in the InternalRel of Q by A1, A2, A3, A4; :: according to ORDERS_2:def 5 :: thesis: verum