consider X being set such that
A3: for x being set 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₁())

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in H₁(F₁()) )
thus ( not x in X or x in H₁(F₁()) ) by A3; :: thesis: verum

end;

then reconsider X = X as non empty Subset of F₁() ;

A4: now

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 SubStrEx1, 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