let n be Nat; for no being Element of OrderedNAT st no = n holds
square-uparrow n = [:(uparrow no),(uparrow no):]
let no be Element of OrderedNAT; ( no = n implies square-uparrow n = [:(uparrow no),(uparrow no):] )
assume A1:
no = n
; square-uparrow n = [:(uparrow no),(uparrow no):]
thus
square-uparrow n c= [:(uparrow no),(uparrow no):]
XBOOLE_0:def 10 [:(uparrow no),(uparrow no):] c= square-uparrow nproof
let x be
object ;
TARSKI:def 3 ( not x in square-uparrow n or x in [:(uparrow no),(uparrow no):] )
assume A3:
x in square-uparrow n
;
x in [:(uparrow no),(uparrow no):]
then reconsider y =
x as
Element of
[:NAT,NAT:] ;
consider n1,
n2 being
Nat such that A4:
n1 = y `1
and A5:
n2 = y `2
and A6:
n <= n1
and A7:
n <= n2
by A3, Def3;
A8:
(
n1 in uparrow no &
n2 in uparrow no )
by A1, A6, A7, Th11;
ex
x1,
x2 being
object st
(
x1 in NAT &
x2 in NAT &
x = [x1,x2] )
by A3, ZFMISC_1:def 2;
then reconsider z =
x as
pair object ;
z = [n1,n2]
by A4, A5;
hence
x in [:(uparrow no),(uparrow no):]
by A8, ZFMISC_1:def 2;
verum
end;
let x be object ; TARSKI:def 3 ( not x in [:(uparrow no),(uparrow no):] or x in square-uparrow n )
assume
x in [:(uparrow no),(uparrow no):]
; x in square-uparrow n
then consider y1, y2 being object such that
A9:
y1 in uparrow no
and
A10:
y2 in uparrow no
and
A11:
x = [y1,y2]
by ZFMISC_1:def 2;
reconsider x = x as Element of [:NAT,NAT:] by A9, A10, A11, ZFMISC_1:def 2;
reconsider y1 = y1, y2 = y2 as Nat by A9, A10;
A12:
( n <= y1 & n <= y2 )
by A1, A9, A10, Th12;
( x `1 = y1 & x `2 = y2 )
by A11;
hence
x in square-uparrow n
by A12, Def3; verum