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, 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_inf_of pi (Y,i),F₂() . i by A5, Th31;
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;
hence ("/\" (X,(product F₂()))) . i is Element of (F₃() . i) by A5, Th33; :: 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