consider X being set such that
A3:
for x being object holds
( x in X iff ( x in H1(F1()) & P1[x] ) )
from XBOOLE_0:sch 1();
reconsider X = X as non empty set by A2, A3;
X c= H1(F1())
by A3;
then reconsider X = X as non empty Subset of F1() ;
A4:
now for x, y being Element of X holds x * y in Xlet x,
y be
Element of
X;
x * y in X
(
P1[
x] &
P1[
y] )
by A3;
then
P1[
x * y]
by A1;
hence
x * y in X
by A3;
verum end;
consider H being non empty strict SubStr of F1() such that
A5:
the carrier of H = X
by Lm5, A4;
take
H
; for x being Element of F1() holds
( x in the carrier of H iff P1[x] )
thus
for x being Element of F1() holds
( x in the carrier of H iff P1[x] )
by A3, A5; verum