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 Def27;
reconsider V = [#] (ConvergenceSpace C) as Subset of S by Def27;
V = the carrier of S by Def27;
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 Th29;
hence the carrier of (ConvergenceSpace C) in the topology of (ConvergenceSpace C) by A1; :: according to PRE_TOPC:def 1 :: thesis:

hereby :: thesis:

let a be Subset-Family of (ConvergenceSpace C); :: thesis:
assume A2: a c= the topology of (ConvergenceSpace C) ; :: thesis:
reconsider V = union a as Subset of S by Def27;

let p be Element of S; :: thesis:
assume p in V ; :: thesis:
then consider X being set such that
A3: p in X and
A4: X in a by TARSKI:def 4;
let N be net of S; :: thesis:
assume A5: [N,p] in C ; :: thesis:
X in the topology of (ConvergenceSpace C) by A2, A4;
then consider W being Subset of S such that
A6: X = W and
A7: 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;
A8: N is_eventually_in X by A3, A5, A6, A7;
X c= V by A4, ZFMISC_1:92;
hence N is_eventually_in V by A8, WAYBEL_0:8; :: thesis:

end;

hence union a in the topology of (ConvergenceSpace C) by A1; :: thesis:

end;

let a, b be Subset of (ConvergenceSpace C); :: thesis:
assume a in the topology of (ConvergenceSpace C) ; :: thesis:
then consider Va being Subset of S such that
A9: a = Va and
A10: 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;
assume b in the topology of (ConvergenceSpace C) ; :: thesis:
then consider Vb being Subset of S such that
A11: b = Vb and
A12: 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;
reconsider V = a /\ b as Subset of S by Def27;

let p be Element of S; :: thesis:
assume A13: p in V ; :: thesis:
let N be net of S; :: thesis:
assume A14: [N,p] in C ; :: thesis:
p in a by A13, XBOOLE_0:def 4;
then N is_eventually_in Va by A9, A10, A14;
then consider i1 being Element of N such that
A15: for j being Element of N st i1 <= j holds
N . j in Va by WAYBEL_0:def 11;
p in b by A13, XBOOLE_0:def 4;
then N is_eventually_in Vb by A11, A12, A14;
then consider i2 being Element of N such that
A16: for j being Element of N st i2 <= j holds
N . j in Vb by WAYBEL_0:def 11;
consider i being Element of N such that
A17: i1 <= i and
A18: i2 <= i by Def5;
thus N is_eventually_in V :: thesis:

take i ; :: according to WAYBEL_0:def 11 :: thesis:
let j be Element of N; :: thesis:
assume A19: i <= j ; :: thesis:
then i1 <= j by A17, YELLOW_0:def 2;
then A20: N . j in Va by A15;
i2 <= j by A18, A19, YELLOW_0:def 2;
then N . j in Vb by A16;
hence N . j in V by A9, A11, A20, XBOOLE_0:def 4; :: thesis:

end;

hence a /\ b in the topology of (ConvergenceSpace C) by A1; :: thesis: