let x be Element of [:base_of_frechet_filter,base_of_frechet_filter:]; :: thesis: ex i, j being Nat st x = [:(NAT \ (Segm i)),(NAT \ (Segm j)):]
x in { [:B1,B2:] where B1, B2 is Element of base_of_frechet_filter : verum } ;
then consider B1, B2 being Element of base_of_frechet_filter such that
A1: x = [:B1,B2:] ;
consider i being Nat such that
A2: B1 = NAT \ (Segm i) by Th20;
consider j being Nat such that
A3: B2 = NAT \ (Segm j) by Th20;
take i ; :: thesis: ex j being Nat st x = [:(NAT \ (Segm i)),(NAT \ (Segm j)):]
take j ; :: thesis: x = [:(NAT \ (Segm i)),(NAT \ (Segm j)):]
thus x = [:(NAT \ (Segm i)),(NAT \ (Segm j)):] by A1, A2, A3; :: thesis: verum