set cB1 = all-square-uparrow ;
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;
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
let 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;
hence all-square-uparrow ,[:base_of_frechet_filter,base_of_frechet_filter:] are_equivalent_generators by A1; :: thesis: verum