reconsider K = F₁() --> F₃(), J = F₁() --> F₂() as non-Empty Poset-yielding ManySortedSet of F₁() ;
A3: for X being Subset of (product K) st P₁[X, product K] holds
for i being Element of F₁() holds P₁[ pi (X,i),K . i] by A1;
A5: for i being Element of F₁()
for X being Subset of (K . i) st P₁[X,K . i] holds
K . i inherits_sup_of X,J . i by A2;
A8: for i being Element of F₁() holds K . i is full SubRelStr of J . i ;
for X being Subset of (product K) st P₁[X, product K] holds
product K inherits_sup_of X, product J from YELLOW16:sch 1(A3, A8, A5);
hence for X being Subset of (F₃() |^ F₁()) st P₁[X,F₃() |^ F₁()] holds
F₃() |^ F₁() inherits_sup_of X,F₂() |^ F₁() ; :: thesis: verum