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 full SubRelStr of J . i ) holds
product K is full 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 full SubRelStr of J . i ) implies product K is full SubRelStr of product J )
assume A1:
for i being Element of I holds K . i is full SubRelStr of J . i
; product K is full SubRelStr of product J
then
for i being Element of I holds K . i is SubRelStr of J . i
;
then reconsider S = product K as non empty SubRelStr of product J by Th35;
A2:
the InternalRel of (product J) |_2 the carrier of S = the InternalRel of (product J) /\ [: the carrier of S, the carrier of S:]
by WELLORD1:def 6;
S is full
proof
the
InternalRel of
S c= the
InternalRel of
(product J)
by YELLOW_0:def 13;
hence
the
InternalRel of
S c= the
InternalRel of
(product J) |_2 the
carrier of
S
by A2, XBOOLE_1:19;
YELLOW_0:def 14,
XBOOLE_0:def 10 K44( the InternalRel of (product J), the carrier of S) c= the InternalRel of S
let x,
y be
object ;
RELAT_1:def 3 ( not [x,y] in K44( the InternalRel of (product J), the carrier of S) or [x,y] in the InternalRel of S )
assume A3:
[x,y] in the
InternalRel of
(product J) |_2 the
carrier of
S
;
[x,y] in the InternalRel of S
then A4:
[x,y] in the
InternalRel of
(product J)
by A2, XBOOLE_0:def 4;
[x,y] in [: the carrier of S, the carrier of S:]
by A2, A3, XBOOLE_0:def 4;
then reconsider x =
x,
y =
y as
Element of
S by ZFMISC_1:87;
reconsider a =
x,
b =
y as
Element of
(product J) by YELLOW_0:58;
reconsider x =
x,
y =
y as
Element of
(product K) ;
A5:
a <= b
by A4, ORDERS_2:def 5;
then
x <= y
by WAYBEL_3:28;
hence
[x,y] in the
InternalRel of
S
by ORDERS_2:def 5;
verum
end;
hence
product K is full SubRelStr of product J
; verum