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

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_sup_of X,F₂() . i