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₃())
set f = "\/" X,(product F₂());
product F₃() is SubRelStr of product F₂() by A2, Th39;
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;
A6: dom ("\/" X,(product F₂())) = F₁() by WAYBEL_3:27;

now

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

end;

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