let X be Subset of (product F3()); ( P1[X, product F3()] implies product F3() inherits_inf_of X, product F2() )
assume that
A4:
P1[X, product F3()]
and
A5:
ex_inf_of X, product F2()
; YELLOW16:def 7 "/\" (X,(product F2())) in the carrier of (product F3())
product F3() is SubRelStr of product F2()
by A2, Th36;
then
the carrier of (product F3()) c= the carrier of (product F2())
by YELLOW_0:def 13;
then reconsider Y = X as Subset of (product F2()) by XBOOLE_1:1;
set f = "/\" (X,(product F2()));
A6:
now for i being Element of F1() holds ("/\" (X,(product F2()))) . i is Element of (F3() . i)let i be
Element of
F1();
("/\" (X,(product F2()))) . i is Element of (F3() . i)A7:
ex_inf_of pi (
Y,
i),
F2()
. i
by A5, Th31;
F3()
. i inherits_inf_of pi (
X,
i),
F2()
. i
by A1, A3, A4;
then
inf (pi (Y,i)) in the
carrier of
(F3() . i)
by A7;
hence
("/\" (X,(product F2()))) . i is
Element of
(F3() . i)
by A5, Th33;
verum end;
dom ("/\" (X,(product F2()))) = F1()
by WAYBEL_3:27;
then
"/\" (X,(product F2())) is Element of (product F3())
by A6, WAYBEL_3:27;
hence
"/\" (X,(product F2())) in the carrier of (product F3())
; verum