let I be non empty set ; for J, K being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds K . i is SubRelStr of J . i ) holds
product K is SubRelStr of product J
let J, K be RelStr-yielding non-Empty ManySortedSet of I; ( ( for i being Element of I holds K . i is SubRelStr of J . i ) implies product K is SubRelStr of product J )
assume A1:
for i being Element of I holds K . i is SubRelStr of J . i
; product K is SubRelStr of product J
A5:
dom (Carrier K) = I
by PARTFUN1:def 2;
A6:
dom (Carrier J) = I
by PARTFUN1:def 2;
A7:
the carrier of (product J) = product (Carrier J)
by YELLOW_1:def 4;
the carrier of (product K) = product (Carrier K)
by YELLOW_1:def 4;
hence A8:
the carrier of (product K) c= the carrier of (product J)
by A7, A6, A5, A2, CARD_3:27; YELLOW_0:def 13 the InternalRel of (product K) c= the InternalRel of (product J)
let x, y be object ; RELAT_1:def 3 ( not [x,y] in the InternalRel of (product K) or [x,y] in the InternalRel of (product J) )
assume A9:
[x,y] in the InternalRel of (product K)
; [x,y] in the InternalRel of (product J)
reconsider x = x, y = y as Element of (product K) by A9, ZFMISC_1:87;
reconsider f = x, g = y as Element of (product J) by A8;
A10:
x <= y
by A9, ORDERS_2:def 5;
then
f <= g
by WAYBEL_3:28;
hence
[x,y] in the InternalRel of (product J)
by ORDERS_2:def 5; verum