consider A being set such that
A1: for x being set holds
( x in A iff ( x in the carrier of (TOP-REAL F₁()) & P₁[x] ) ) from XBOOLE_0:sch 1();
A c= the carrier of (TOP-REAL F₁())

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in the carrier of (TOP-REAL F₁()) )
assume x in A ; :: thesis: x in the carrier of (TOP-REAL F₁())
hence x in the carrier of (TOP-REAL F₁()) by A1; :: thesis: verum

end;

then reconsider A = A as Subset of (TOP-REAL F₁()) ;
take A ; :: thesis: for p being Point of (TOP-REAL F₁()) holds
( p in A iff P₁[p] )
thus for p being Point of (TOP-REAL F₁()) holds
( p in A iff P₁[p] ) by A1; :: thesis: verum