let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of (TOP-REAL 2) : ( P₁[p] & p <> 0. (TOP-REAL 2) ) } or x in the carrier of ((TOP-REAL 2) | F₁()) )
A2: F₁() ` = {(0. (TOP-REAL 2))} by A1, JGRAPH_3:30;
assume x in { p where p is Point of (TOP-REAL 2) : ( P₁[p] & p <> 0. (TOP-REAL 2) ) } ; :: thesis: x in the carrier of ((TOP-REAL 2) | F₁())
then consider p being Point of (TOP-REAL 2) such that
A3: ( x = p & P₁[p] & p <> 0. (TOP-REAL 2) ) ;

now

assume not x in F₁() ; :: thesis: contradiction
then x in the carrier of (TOP-REAL 2) \ F₁() by A3, XBOOLE_0:def 5;
then x in F₁() ` by SUBSET_1:def 5;
hence contradiction by A2, A3, TARSKI:def 1; :: thesis: verum

end;

hence x in the carrier of ((TOP-REAL 2) | F₁()) by PRE_TOPC:29; :: thesis: verum