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 }

proof

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 }

proof

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;

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

end;

square-uparrow 1 in { (square-uparrow 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

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:]

proof

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;

hence contradiction by A7, COMBGRAS:5, Th9; :: thesis: verum

end;