let T be non empty TopSpace; :: thesis: for F being proper Filter of (BoolePoset ([#] T))

for x being Point of T holds

( x is_a_cluster_point_of a_net F iff x is_a_cluster_point_of F,T )

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

( x is_a_cluster_point_of a_net F iff x is_a_cluster_point_of F,T )

F = a_filter (a_net F) by Th14;

hence for x being Point of T holds

( x is_a_cluster_point_of a_net F iff x is_a_cluster_point_of F,T ) by Th11; :: thesis: verum

for x being Point of T holds

( x is_a_cluster_point_of a_net F iff x is_a_cluster_point_of F,T )

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

( x is_a_cluster_point_of a_net F iff x is_a_cluster_point_of F,T )

F = a_filter (a_net F) by Th14;

hence for x being Point of T holds

( x is_a_cluster_point_of a_net F iff x is_a_cluster_point_of F,T ) by Th11; :: thesis: verum