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 ) )

proof

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;

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 C1 holds
N is_eventually_in V } ;
hence A in the topology of (ConvergenceSpace C1) by YELLOW_6:def 24; :: thesis: verum