let L be non empty 1-sorted ; :: thesis: for C1, C2 being Convergence-Class of L st C1 c= C2 holds

the topology of (ConvergenceSpace C2) c= the topology of (ConvergenceSpace C1)

let C1, C2 be Convergence-Class of L; :: thesis: ( C1 c= C2 implies the topology of (ConvergenceSpace C2) c= the topology of (ConvergenceSpace C1) )

assume A1: C1 c= C2 ; :: thesis: the topology of (ConvergenceSpace C2) c= the topology of (ConvergenceSpace C1)

let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in the topology of (ConvergenceSpace C2) or A in the topology of (ConvergenceSpace C1) )

assume A in the topology of (ConvergenceSpace C2) ; :: thesis: A in the topology of (ConvergenceSpace C1)

then A in { V where V is Subset of L : for p being Element of L st p in V holds

for N being net of L st [N,p] in C2 holds

N is_eventually_in V } by YELLOW_6:def 24;

then consider V1 being Subset of L such that

A2: A = V1 and

A3: for p being Element of L st p in V1 holds

for N being net of L st [N,p] in C2 holds

N is_eventually_in V1 ;

ex V being Subset of L st

( A = V & ( for p being Element of L st p in V holds

for N being net of L st [N,p] in C1 holds

N is_eventually_in V ) )

for N being net of L st [N,p] in C1 holds

N is_eventually_in V } ;

hence A in the topology of (ConvergenceSpace C1) by YELLOW_6:def 24; :: thesis: verum

the topology of (ConvergenceSpace C2) c= the topology of (ConvergenceSpace C1)

let C1, C2 be Convergence-Class of L; :: thesis: ( C1 c= C2 implies the topology of (ConvergenceSpace C2) c= the topology of (ConvergenceSpace C1) )

assume A1: C1 c= C2 ; :: thesis: the topology of (ConvergenceSpace C2) c= the topology of (ConvergenceSpace C1)

let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in the topology of (ConvergenceSpace C2) or A in the topology of (ConvergenceSpace C1) )

assume A in the topology of (ConvergenceSpace C2) ; :: thesis: A in the topology of (ConvergenceSpace C1)

then A in { V where V is Subset of L : for p being Element of L st p in V holds

for N being net of L st [N,p] in C2 holds

N is_eventually_in V } by YELLOW_6:def 24;

then consider V1 being Subset of L such that

A2: A = V1 and

A3: for p being Element of L st p in V1 holds

for N being net of L st [N,p] in C2 holds

N is_eventually_in V1 ;

ex V being Subset of L st

( A = V & ( for p being Element of L st p in V holds

for N being net of L st [N,p] in C1 holds

N is_eventually_in V ) )

proof

then
A in { V where V is Subset of L : for p being Element of L st p in V holds
take
V1
; :: thesis: ( A = V1 & ( for p being Element of L st p in V1 holds

for N being net of L st [N,p] in C1 holds

N is_eventually_in V1 ) )

thus A = V1 by A2; :: thesis: for p being Element of L st p in V1 holds

for N being net of L st [N,p] in C1 holds

N is_eventually_in V1

let p be Element of L; :: thesis: ( p in V1 implies for N being net of L st [N,p] in C1 holds

N is_eventually_in V1 )

assume A4: p in V1 ; :: thesis: for N being net of L st [N,p] in C1 holds

N is_eventually_in V1

let N be net of L; :: thesis: ( [N,p] in C1 implies N is_eventually_in V1 )

assume [N,p] in C1 ; :: thesis: N is_eventually_in V1

hence N is_eventually_in V1 by A1, A3, A4; :: thesis: verum

end;for N being net of L st [N,p] in C1 holds

N is_eventually_in V1 ) )

thus A = V1 by A2; :: thesis: for p being Element of L st p in V1 holds

for N being net of L st [N,p] in C1 holds

N is_eventually_in V1

let p be Element of L; :: thesis: ( p in V1 implies for N being net of L st [N,p] in C1 holds

N is_eventually_in V1 )

assume A4: p in V1 ; :: thesis: for N being net of L st [N,p] in C1 holds

N is_eventually_in V1

let N be net of L; :: thesis: ( [N,p] in C1 implies N is_eventually_in V1 )

assume [N,p] in C1 ; :: thesis: N is_eventually_in V1

hence N is_eventually_in V1 by A1, A3, A4; :: thesis: verum

for N being net of L st [N,p] in C1 holds

N is_eventually_in V } ;

hence A in the topology of (ConvergenceSpace C1) by YELLOW_6:def 24; :: thesis: verum