let X be Subset of (product F₃()); :: thesis: ( P₁[X, product F₃()] implies product F₃() inherits_sup_of X, product F₂() )
assume that
A4: P₁[X, product F₃()] and
A5: ex_sup_of X, product F₂() ; :: according to YELLOW16:def 6 :: thesis: "\/" (X,(product F₂())) in the carrier of (product F₃())
product F₃() is SubRelStr of product F₂() by A2, Th36;
then the carrier of (product F₃()) c= the carrier of (product F₂()) by YELLOW_0:def 13;
then reconsider Y = X as Subset of (product F₂()) by XBOOLE_1:1;
set f = "\/" (X,(product F₂()));

A6: now :: thesis: for i being Element of F₁() holds ("\/" (X,(product F₂()))) . i is Element of (F₃() . i)

let i be Element of F₁(); :: thesis: ("\/" (X,(product F₂()))) . i is Element of (F₃() . i)
A7: ex_sup_of pi (Y,i),F₂() . i by A5, Th30;
F₃() . i inherits_sup_of pi (X,i),F₂() . i by A1, A3, A4;
then sup (pi (Y,i)) in the carrier of (F₃() . i) by A7;
hence ("\/" (X,(product F₂()))) . i is Element of (F₃() . i) by A5, Th32; :: thesis: verum

end;

dom ("\/" (X,(product F₂()))) = F₁() by WAYBEL_3:27;
then "\/" (X,(product F₂())) is Element of (product F₃()) by A6, WAYBEL_3:27;
hence "\/" (X,(product F₂())) in the carrier of (product F₃()) ; :: thesis: verum