let x be object ; :: 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₁()) )
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 A2: ex p being Point of (TOP-REAL 2) st
( x = p & P₁[p] & p <> 0. (TOP-REAL 2) ) ;
A3: F₁() ` = {(0. (TOP-REAL 2))} by A1, JGRAPH_3:20;

now :: thesis: x in F₁()

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

end;

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