let T be non empty TopSpace; :: thesis: for A being Subset of T holds
( A is closed iff for F being ultra Filter of (BoolePoset ([#] T)) st A in F holds
for x being Point of T st x is_a_convergence_point_of F,T holds
x in A )
let A be Subset of T; :: thesis: ( A is closed iff for F being ultra Filter of (BoolePoset ([#] T)) st A in F holds
for x being Point of T st x is_a_convergence_point_of F,T holds
x in A )
( A is closed iff Cl A = A ) by PRE_TOPC:22;
hence ( A is closed implies for F being ultra Filter of (BoolePoset ([#] T)) st A in F holds
for x being Point of T st x is_a_convergence_point_of F,T holds
x in A ) by Th26; :: thesis: ( ( for F being ultra Filter of (BoolePoset ([#] T)) st A in F holds
for x being Point of T st x is_a_convergence_point_of F,T holds
x in A ) implies A is closed )
assume A1: for F being ultra Filter of (BoolePoset ([#] T)) st A in F holds
for x being Point of T st x is_a_convergence_point_of F,T holds
x in A ; :: thesis: A is closed
A = Cl A
proof
thus A c= Cl A by PRE_TOPC:18; :: according to XBOOLE_0:def 10 :: thesis: Cl A c= A
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Cl A or x in A )
assume A2: x in Cl A ; :: thesis: x in A
then reconsider y = x as Element of T ;
ex F being ultra Filter of (BoolePoset ([#] T)) st
( A in F & y is_a_convergence_point_of F,T ) by A2, Th26;
hence x in A by A1; :: thesis: verum
end;
hence A is closed ; :: thesis: verum