let T be non empty TopSpace; :: thesis: for x being Point of T

for F being upper Subset of (BoolePoset ([#] T)) holds

( x is_a_convergence_point_of F,T iff NeighborhoodSystem x c= F )

let x be Point of T; :: thesis: for F being upper Subset of (BoolePoset ([#] T)) holds

( x is_a_convergence_point_of F,T iff NeighborhoodSystem x c= F )

let F be upper Subset of (BoolePoset ([#] T)); :: thesis: ( x is_a_convergence_point_of F,T iff NeighborhoodSystem x c= F )

let A be Subset of T; :: according to WAYBEL_7:def 5 :: thesis: ( not A is open or not x in A or A in F )

assume that

A4: A is open and

A5: x in A ; :: thesis: A in F

A is a_neighborhood of x by A4, A5, CONNSP_2:3;

then A in NeighborhoodSystem x ;

hence A in F by A3; :: thesis: verum

for F being upper Subset of (BoolePoset ([#] T)) holds

( x is_a_convergence_point_of F,T iff NeighborhoodSystem x c= F )

let x be Point of T; :: thesis: for F being upper Subset of (BoolePoset ([#] T)) holds

( x is_a_convergence_point_of F,T iff NeighborhoodSystem x c= F )

let F be upper Subset of (BoolePoset ([#] T)); :: thesis: ( x is_a_convergence_point_of F,T iff NeighborhoodSystem x c= F )

hereby :: thesis: ( NeighborhoodSystem x c= F implies x is_a_convergence_point_of F,T )

assume A3:
NeighborhoodSystem x c= F
; :: thesis: x is_a_convergence_point_of F,Tassume A1:
x is_a_convergence_point_of F,T
; :: thesis: NeighborhoodSystem x c= F

thus NeighborhoodSystem x c= F :: thesis: verum

end;thus NeighborhoodSystem x c= F :: thesis: verum

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in NeighborhoodSystem x or y in F )

assume y in NeighborhoodSystem x ; :: thesis: y in F

then reconsider y = y as a_neighborhood of x by Th2;

x in Int y by CONNSP_2:def 1;

then A2: Int y in F by A1;

Int y c= y by TOPS_1:16;

hence y in F by A2, WAYBEL_7:7; :: thesis: verum

end;assume y in NeighborhoodSystem x ; :: thesis: y in F

then reconsider y = y as a_neighborhood of x by Th2;

x in Int y by CONNSP_2:def 1;

then A2: Int y in F by A1;

Int y c= y by TOPS_1:16;

hence y in F by A2, WAYBEL_7:7; :: thesis: verum

let A be Subset of T; :: according to WAYBEL_7:def 5 :: thesis: ( not A is open or not x in A or A in F )

assume that

A4: A is open and

A5: x in A ; :: thesis: A in F

A is a_neighborhood of x by A4, A5, CONNSP_2:3;

then A in NeighborhoodSystem x ;

hence A in F by A3; :: thesis: verum