set IT = ConvergenceSpace C;
A1:
the topology of (ConvergenceSpace C) = { V where V is Subset of S : for p being Element of S st p in V holds
for N being net of S st [N,p] in C holds
N is_eventually_in V }
by Def24;
reconsider V = [#] (ConvergenceSpace C) as Subset of S by Def24;
V = the carrier of S
by Def24;
then
for p being Element of S st p in V holds
for N being net of S st [N,p] in C holds
N is_eventually_in V
by Th20;
hence
the carrier of (ConvergenceSpace C) in the topology of (ConvergenceSpace C)
by A1; PRE_TOPC:def 1 ( ( for b1 being Element of bool (bool the carrier of (ConvergenceSpace C)) holds
( not b1 c= the topology of (ConvergenceSpace C) or union b1 in the topology of (ConvergenceSpace C) ) ) & ( for b1, b2 being Element of bool the carrier of (ConvergenceSpace C) holds
( not b1 in the topology of (ConvergenceSpace C) or not b2 in the topology of (ConvergenceSpace C) or b1 /\ b2 in the topology of (ConvergenceSpace C) ) ) )
hereby for b1, b2 being Element of bool the carrier of (ConvergenceSpace C) holds
( not b1 in the topology of (ConvergenceSpace C) or not b2 in the topology of (ConvergenceSpace C) or b1 /\ b2 in the topology of (ConvergenceSpace C) )
let a be
Subset-Family of
(ConvergenceSpace C);
( a c= the topology of (ConvergenceSpace C) implies union a in the topology of (ConvergenceSpace C) )assume A2:
a c= the
topology of
(ConvergenceSpace C)
;
union a in the topology of (ConvergenceSpace C)reconsider V =
union a as
Subset of
S by Def24;
now for p being Element of S st p in V holds
for N being net of S st [N,p] in C holds
N is_eventually_in Vlet p be
Element of
S;
( p in V implies for N being net of S st [N,p] in C holds
N is_eventually_in V )assume
p in V
;
for N being net of S st [N,p] in C holds
N is_eventually_in Vthen consider X being
set such that A3:
p in X
and A4:
X in a
by TARSKI:def 4;
A5:
X c= V
by A4, ZFMISC_1:74;
X in the
topology of
(ConvergenceSpace C)
by A2, A4;
then A6:
ex
W being
Subset of
S st
(
X = W & ( for
p being
Element of
S st
p in W holds
for
N being
net of
S st
[N,p] in C holds
N is_eventually_in W ) )
by A1;
let N be
net of
S;
( [N,p] in C implies N is_eventually_in V )assume
[N,p] in C
;
N is_eventually_in Vhence
N is_eventually_in V
by A3, A6, A5, WAYBEL_0:8;
verum end; hence
union a in the
topology of
(ConvergenceSpace C)
by A1;
verum
end;
let a, b be Subset of (ConvergenceSpace C); ( not a in the topology of (ConvergenceSpace C) or not b in the topology of (ConvergenceSpace C) or a /\ b in the topology of (ConvergenceSpace C) )
assume
a in the topology of (ConvergenceSpace C)
; ( not b in the topology of (ConvergenceSpace C) or a /\ b in the topology of (ConvergenceSpace C) )
then consider Va being Subset of S such that
A7:
a = Va
and
A8:
for p being Element of S st p in Va holds
for N being net of S st [N,p] in C holds
N is_eventually_in Va
by A1;
reconsider V = a /\ b as Subset of S by Def24;
assume
b in the topology of (ConvergenceSpace C)
; a /\ b in the topology of (ConvergenceSpace C)
then consider Vb being Subset of S such that
A9:
b = Vb
and
A10:
for p being Element of S st p in Vb holds
for N being net of S st [N,p] in C holds
N is_eventually_in Vb
by A1;
now for p being Element of S st p in V holds
for N being net of S st [N,p] in C holds
N is_eventually_in Vlet p be
Element of
S;
( p in V implies for N being net of S st [N,p] in C holds
N is_eventually_in V )assume A11:
p in V
;
for N being net of S st [N,p] in C holds
N is_eventually_in Vlet N be
net of
S;
( [N,p] in C implies N is_eventually_in V )assume A12:
[N,p] in C
;
N is_eventually_in V
p in b
by A11, XBOOLE_0:def 4;
then
N is_eventually_in Vb
by A9, A10, A12;
then consider i2 being
Element of
N such that A13:
for
j being
Element of
N st
i2 <= j holds
N . j in Vb
;
p in a
by A11, XBOOLE_0:def 4;
then
N is_eventually_in Va
by A7, A8, A12;
then consider i1 being
Element of
N such that A14:
for
j being
Element of
N st
i1 <= j holds
N . j in Va
;
consider i being
Element of
N such that A15:
i1 <= i
and A16:
i2 <= i
by Def3;
thus
N is_eventually_in V
verum end;
hence
a /\ b in the topology of (ConvergenceSpace C)
by A1; verum