let X be Subset of (product F₃()); :: thesis: ( P₁[X, product F₃()] implies product F₃() inherits_inf_of X, product F₂() )
assume that
A4: P₁[X, product F₃()] and
A5: ex_inf_of X, product F₂() ; :: according to YELLOW16:def 7 :: thesis: "/\" X,(product F₂()) in the carrier of (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;
set f = "/\" X,(product F₂());

A6: now

let i be Element of F₁(); :: thesis: ("/\" X,(product F₂())) . i is Element of (F₃() . i)
A7: ex_inf_of pi Y,i,F₂() . i by A5, Th34;
F₃() . i inherits_inf_of pi X,i,F₂() . i by A1, A3, A4;
then inf (pi Y,i) in the carrier of (F₃() . i) by A7, Def7;
hence ("/\" X,(product F₂())) . i is Element of (F₃() . i) by A5, Th36; :: 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