consider A being set such that
A1: for x being object 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₁()) by A1;
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