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

let C1, C2 be Convergence-Class of L; :: thesis: ( C1 c= C2 implies the topology of () c= the topology of () )
assume A1: C1 c= C2 ; :: thesis: the topology of () c= the topology of ()
let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in the topology of () or A in the topology of () )
assume A in the topology of () ; :: thesis: A in the topology of ()
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:
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 () by YELLOW_6:def 24; :: thesis: verum