scheme :: YELLOW16:sch 3
ProductInfsInheriting{ F₁() -> non empty set , F₂() -> non-Empty Poset-yielding ManySortedSet of F₁(), F₃() -> non-Empty Poset-yielding ManySortedSet of F₁(), P₁[ set , set ] } :

for X being Subset of (product F₃()) st P₁[X, product F₃()] holds
product F₃() inherits_inf_of X, product F₂()

provided

A1: for X being Subset of (product F₃()) st P₁[X, product F₃()] holds
for i being Element of F₁() holds P₁[ pi (X,i),F₃() . i] and
A2: for i being Element of F₁() holds F₃() . i is full SubRelStr of F₂() . i and
A3: for i being Element of F₁()
for X being Subset of (F₃() . i) st P₁[X,F₃() . i] holds
F₃() . i inherits_inf_of X,F₂() . i