set cB1 = all-square-uparrow ;

set cB2 = [:base_of_frechet_filter,base_of_frechet_filter:];

set cB2 = [:base_of_frechet_filter,base_of_frechet_filter:];

A1: now :: thesis: for b1 being Element of all-square-uparrow ex b2 being Element of [:base_of_frechet_filter,base_of_frechet_filter:] st b2 c= b1

let b1 be Element of all-square-uparrow ; :: thesis: ex b2 being Element of [:base_of_frechet_filter,base_of_frechet_filter:] st b2 c= b1

b1 in all-square-uparrow ;

then consider n being Nat such that

A2: b1 = square-uparrow n ;

NAT \ (Segm n) is Element of base_of_frechet_filter by Th21;

then [:(NAT \ (Segm n)),(NAT \ (Segm n)):] in [:base_of_frechet_filter,base_of_frechet_filter:] ;

then reconsider b2 = [:(NAT \ (Segm n)),(NAT \ (Segm n)):] as Element of [:base_of_frechet_filter,base_of_frechet_filter:] ;

b2 c= b1 by A2, Th27;

hence ex b2 being Element of [:base_of_frechet_filter,base_of_frechet_filter:] st b2 c= b1 ; :: thesis: verum

end;b1 in all-square-uparrow ;

then consider n being Nat such that

A2: b1 = square-uparrow n ;

NAT \ (Segm n) is Element of base_of_frechet_filter by Th21;

then [:(NAT \ (Segm n)),(NAT \ (Segm n)):] in [:base_of_frechet_filter,base_of_frechet_filter:] ;

then reconsider b2 = [:(NAT \ (Segm n)),(NAT \ (Segm n)):] as Element of [:base_of_frechet_filter,base_of_frechet_filter:] ;

b2 c= b1 by A2, Th27;

hence ex b2 being Element of [:base_of_frechet_filter,base_of_frechet_filter:] st b2 c= b1 ; :: thesis: verum

now :: thesis: for b2 being Element of [:base_of_frechet_filter,base_of_frechet_filter:] ex b1 being Element of all-square-uparrow st b1 c= b2

hence
all-square-uparrow ,[:base_of_frechet_filter,base_of_frechet_filter:] are_equivalent_generators
by A1; :: thesis: verumlet b2 be Element of [:base_of_frechet_filter,base_of_frechet_filter:]; :: thesis: ex b1 being Element of all-square-uparrow st b1 c= b2

consider n being Nat such that

A1: square-uparrow n c= b2 by Th32;

square-uparrow n in all-square-uparrow ;

hence ex b1 being Element of all-square-uparrow st b1 c= b2 by A1; :: thesis: verum

end;consider n being Nat such that

A1: square-uparrow n c= b2 by Th32;

square-uparrow n in all-square-uparrow ;

hence ex b1 being Element of all-square-uparrow st b1 c= b2 by A1; :: thesis: verum