consider X being set such that
A3: for x being object holds
( x in X iff ( x in H₁(F₁()) & P₁[x] ) ) from XBOOLE_0:sch 1();
reconsider X = X as non empty set by A2, A3;
X c= H₁(F₁()) by A3;
then reconsider X = X as non empty Subset of F₁() ;

A4: now :: thesis: for x, y being Element of X holds x * y in X

let x, y be Element of X; :: thesis: x * y in X
( P₁[x] & P₁[y] ) by A3;
then P₁[x * y] by A1;
hence x * y in X by A3; :: thesis: verum

end;

consider H being non empty strict SubStr of F₁() such that
A5: the carrier of H = X by Lm5, A4;
take H ; :: thesis: for x being Element of F₁() holds
( x in the carrier of H iff P₁[x] )
thus for x being Element of F₁() holds
( x in the carrier of H iff P₁[x] ) by A3, A5; :: thesis: verum