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

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