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

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

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 [:(uparrow no),(uparrow no):] or x in square-uparrow n )
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;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

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