theorem :: PCS_0:8

for P, Q being RelStr
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 ;