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 ;
TARSKI:def 3 ( not x in square-uparrow 1 or x in [:NAT,NAT:] \ { [0,n] where n is Nat : verum } )
assume
x in square-uparrow 1
;
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 }
hence
x in [:NAT,NAT:] \ { [0,n] where n is Nat : verum }
by A5, XBOOLE_0:def 5;
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; 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:]
verumproof
assume
[:NAT,NAT:] \ { [0,n] where n is Nat : verum } in Frechet_Filter [:NAT,NAT:]
;
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:]
hence
contradiction
by A7, COMBGRAS:5, Th9;
verum
end;