thus F₁() ` c= { p where p is Point of (TOP-REAL 2) : P<sub>1</sub>[p] } :: according to XBOOLE_0:def 10 :: thesis: { p where p is Point of (TOP-REAL 2) : P<sub>1</sub>[p] } c= F<sub>1</sub>() `

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F₁() ` or x in { p where p is Point of (TOP-REAL 2) : P<sub>1</sub>[p] } )
assume A2: x in F<sub>1</sub>() ` ; :: thesis: x in { p where p is Point of (TOP-REAL 2) : P₁[p] }
then reconsider qx = x as Point of (TOP-REAL 2) ;
x in the carrier of (TOP-REAL 2) \ F₁() by A2, SUBSET_1:def 4;
then not x in F₁() by XBOOLE_0:def 5;
then P₁[qx] by A1;
hence x in { p where p is Point of (TOP-REAL 2) : P₁[p] } ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of (TOP-REAL 2) : P₁[p] } or x in F₁() ` )
assume x in { p7 where p7 is Point of (TOP-REAL 2) : P<sub>1</sub>[p7] } ; :: thesis: x in F<sub>1</sub>() `
then A3: ex p7 being Point of (TOP-REAL 2) st
( p7 = x & P₁[p7] ) ;
then for q7 being Point of (TOP-REAL 2) holds
( not x = q7 or not P₁[q7] ) ;
then not x in F₁() by A1;
then x in the carrier of (TOP-REAL 2) \ F₁() by A3, XBOOLE_0:def 5;
hence x in F₁() ` by SUBSET_1:def 4; :: thesis: verum