set cB1 = all-square-uparrow ;
set cB2 = ;
A1: now :: thesis: for b1 being Element of all-square-uparrow ex b2 being Element of st b2 c= b1
let b1 be Element of all-square-uparrow ; :: thesis: ex b2 being Element of 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 ;
then reconsider b2 = [:(NAT \ (Segm n)),(NAT \ (Segm n)):] as Element of ;
b2 c= b1 by ;
hence ex b2 being Element of st b2 c= b1 ; :: thesis: verum
end;
now :: thesis: for b2 being Element of ex b1 being Element of all-square-uparrow st b1 c= b2
let b2 be Element of ; :: 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 , are_equivalent_generators by A1; :: thesis: verum