let T be non empty 1-sorted ; :: thesis: for C being topological Convergence-Class of T
for S being Subset of (ConvergenceSpace C) holds
( S is closed iff for p being Element of T
for N being net of T st [N,p] in C & N is_often_in S holds
p in S )
let C be topological Convergence-Class of T; :: thesis: for S being Subset of (ConvergenceSpace C) holds
( S is closed iff for p being Element of T
for N being net of T st [N,p] in C & N is_often_in S holds
p in S )
let S be Subset of (ConvergenceSpace C); :: thesis: ( S is closed iff for p being Element of T
for N being net of T st [N,p] in C & N is_often_in S holds
p in S )
set CC = ConvergenceSpace C;
A1: the carrier of T = the carrier of (ConvergenceSpace C) by Def24;
hereby :: thesis: ( ( for p being Element of T
for N being net of T st [N,p] in C & N is_often_in S holds
p in S ) implies S is closed )
assume S is closed ; :: thesis: for p being Element of T
for N being net of T st [N,p] in C & N is_often_in S holds
p in S
then A2: S ` is open ;
let p be Element of T; :: thesis: for N being net of T st [N,p] in C & N is_often_in S holds
p in S
let N be net of T; :: thesis: ( [N,p] in C & N is_often_in S implies p in S )
assume A3: [N,p] in C ; :: thesis: ( N is_often_in S implies p in S )
assume N is_often_in S ; :: thesis: p in S
then not N is_eventually_in ([#] (ConvergenceSpace C)) \ S by A1, WAYBEL_0:10;
then not p in S ` by A3, A2, Th41;
hence p in S by A1, XBOOLE_0:def 5; :: thesis: verum
end;
assume A4: for p being Element of T
for N being net of T st [N,p] in C & N is_often_in S holds
p in S ; :: thesis: S is closed
now :: thesis: for p being Element of T st p in S ` holds
for N being net of T st [N,p] in C holds
N is_eventually_in S `
let p be Element of T; :: thesis: ( p in S ` implies for N being net of T st [N,p] in C holds
N is_eventually_in S ` )
assume p in S ` ; :: thesis: for N being net of T st [N,p] in C holds
N is_eventually_in S `
then A5: not p in S by XBOOLE_0:def 5;
let N be net of T; :: thesis: ( [N,p] in C implies N is_eventually_in S ` )
assume [N,p] in C ; :: thesis: N is_eventually_in S `
then not N is_often_in S by A4, A5;
hence N is_eventually_in S ` by A1, WAYBEL_0:10; :: thesis: verum
end;
then S ` is open by Th41;
hence S is closed ; :: thesis: verum