let n be Nat; :: thesis: for no being Element of OrderedNAT st no = n holds
square-uparrow n = [:(uparrow no),(uparrow no):]
let no be Element of OrderedNAT; :: thesis: ( no = n implies square-uparrow n = [:(uparrow no),(uparrow no):] )
assume A1: no = n ; :: thesis: square-uparrow n = [:(uparrow no),(uparrow no):]
thus square-uparrow n c= [:(uparrow no),(uparrow no):] :: according to XBOOLE_0:def 10 :: thesis: [:(uparrow no),(uparrow no):] c= square-uparrow n

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in square-uparrow n or x in [:(uparrow no),(uparrow no):] )
assume A3: x in square-uparrow n ; :: thesis: 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; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [:(uparrow no),(uparrow no):] or x in square-uparrow n )
assume x in [:(uparrow no),(uparrow no):] ; :: thesis: 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; :: thesis: verum