set X = [:NAT,NAT:] \ { [0,n] where n is Nat : verum } ;

A1: square-uparrow 1 c= [:NAT,NAT:] \ { [0,n] where n is Nat : verum }

hence [:NAT,NAT:] \ { [0,n] where n is Nat : verum } in <.(Frechet_Filter NAT),(Frechet_Filter NAT).) by A1, CARDFIL2:def 8, Th36; :: thesis: not [:NAT,NAT:] \ { [0,n] where n is Nat : verum } in Frechet_Filter [:NAT,NAT:]

thus not [:NAT,NAT:] \ { [0,n] where n is Nat : verum } in Frechet_Filter [:NAT,NAT:] :: thesis: verum

A1: square-uparrow 1 c= [:NAT,NAT:] \ { [0,n] where n is Nat : verum }

proof

square-uparrow 1 in { (square-uparrow n) where n is Nat : verum }
;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in square-uparrow 1 or x in [:NAT,NAT:] \ { [0,n] where n is Nat : verum } )

assume x in square-uparrow 1 ; :: thesis: x in [:NAT,NAT:] \ { [0,n] where n is Nat : verum }

then x in [:(NAT \ (Segm 1)),(NAT \ (Segm 1)):] by Th27;

then consider n, m being object such that

A2: n in NAT \ (Segm 1) and

A3: m in NAT \ (Segm 1) and

A4: x = [n,m] by ZFMISC_1:def 2;

reconsider n = n, m = m as Nat by A2, A3;

A5: x in [:NAT,NAT:] by A4, A2, A3, ZFMISC_1:def 2;

not n in Segm 1 by A2, XBOOLE_0:def 5;

then A6: not n = 0 by NAT_1:44;

not x in { [0,n] where n is Nat : verum }

end;assume x in square-uparrow 1 ; :: thesis: x in [:NAT,NAT:] \ { [0,n] where n is Nat : verum }

then x in [:(NAT \ (Segm 1)),(NAT \ (Segm 1)):] by Th27;

then consider n, m being object such that

A2: n in NAT \ (Segm 1) and

A3: m in NAT \ (Segm 1) and

A4: x = [n,m] by ZFMISC_1:def 2;

reconsider n = n, m = m as Nat by A2, A3;

A5: x in [:NAT,NAT:] by A4, A2, A3, ZFMISC_1:def 2;

not n in Segm 1 by A2, XBOOLE_0:def 5;

then A6: not n = 0 by NAT_1:44;

not x in { [0,n] where n is Nat : verum }

proof

hence
x in [:NAT,NAT:] \ { [0,n] where n is Nat : verum }
by A5, XBOOLE_0:def 5; :: thesis: verum
assume
x in { [0,n] where n is Nat : verum }
; :: thesis: contradiction

then ex k being Nat st x = [0,k] ;

hence contradiction by A6, A4, XTUPLE_0:1; :: thesis: verum

end;then ex k being Nat st x = [0,k] ;

hence contradiction by A6, A4, XTUPLE_0:1; :: thesis: verum

hence [:NAT,NAT:] \ { [0,n] where n is Nat : verum } in <.(Frechet_Filter NAT),(Frechet_Filter NAT).) by A1, CARDFIL2:def 8, Th36; :: thesis: not [:NAT,NAT:] \ { [0,n] where n is Nat : verum } in Frechet_Filter [:NAT,NAT:]

thus not [:NAT,NAT:] \ { [0,n] where n is Nat : verum } in Frechet_Filter [:NAT,NAT:] :: thesis: verum

proof

assume
[:NAT,NAT:] \ { [0,n] where n is Nat : verum } in Frechet_Filter [:NAT,NAT:]
; :: thesis: contradiction

then [:NAT,NAT:] \ { [0,n] where n is Nat : verum } in { ([:NAT,NAT:] \ A) where A is finite Subset of [:NAT,NAT:] : verum } by CARDFIL2:51;

then consider A being finite Subset of [:NAT,NAT:] such that

A7: [:NAT,NAT:] \ { [0,n] where n is Nat : verum } = [:NAT,NAT:] \ A ;

{ [0,n] where n is Nat : verum } c= [:NAT,NAT:]

end;then [:NAT,NAT:] \ { [0,n] where n is Nat : verum } in { ([:NAT,NAT:] \ A) where A is finite Subset of [:NAT,NAT:] : verum } by CARDFIL2:51;

then consider A being finite Subset of [:NAT,NAT:] such that

A7: [:NAT,NAT:] \ { [0,n] where n is Nat : verum } = [:NAT,NAT:] \ A ;

{ [0,n] where n is Nat : verum } c= [:NAT,NAT:]

proof

hence
contradiction
by A7, COMBGRAS:5, Th9; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [0,n] where n is Nat : verum } or x in [:NAT,NAT:] )

assume x in { [0,n] where n is Nat : verum } ; :: thesis: x in [:NAT,NAT:]

then consider n being Nat such that

A8: x = [0,n] ;

( n in NAT & 0 in NAT ) by ORDINAL1:def 12;

hence x in [:NAT,NAT:] by A8, ZFMISC_1:def 2; :: thesis: verum

end;assume x in { [0,n] where n is Nat : verum } ; :: thesis: x in [:NAT,NAT:]

then consider n being Nat such that

A8: x = [0,n] ;

( n in NAT & 0 in NAT ) by ORDINAL1:def 12;

hence x in [:NAT,NAT:] by A8, ZFMISC_1:def 2; :: thesis: verum