set X = \ { [0,n] where n is Nat : verum } ;
A1: square-uparrow 1 c= \ { [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 \ { [0,n] where n is Nat : verum } )
assume x in square-uparrow 1 ; :: thesis: x in \ { [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 by ;
not n in Segm 1 by ;
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 \ { [0,n] where n is Nat : verum } by ; :: thesis: verum
end;
square-uparrow 1 in { () where n is Nat : verum } ;
hence [::] \ { [0,n] where n is Nat : verum } in by ; :: thesis: not \ { [0,n] where n is Nat : verum } in Frechet_Filter
thus not [::] \ { [0,n] where n is Nat : verum } in Frechet_Filter :: thesis: verum
proof
assume [::] \ { [0,n] where n is Nat : verum } in Frechet_Filter ; :: thesis: contradiction
then [::] \ { [0,n] where n is Nat : verum } in { () where A is finite Subset of : verum } by CARDFIL2:51;
then consider A being finite Subset of such that
A7: [::] \ { [0,n] where n is Nat : verum } = \ A ;
{ [0,n] where n is Nat : verum } c=
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [0,n] where n is Nat : verum } or x in )
assume x in { [0,n] where n is Nat : verum } ; :: thesis:
then consider n being Nat such that
A8: x = [0,n] ;
( n in NAT & 0 in NAT ) by ORDINAL1:def 12;
hence x in by ; :: thesis: verum
end;
hence contradiction by A7, COMBGRAS:5, Th9; :: thesis: verum
end;