let n be Nat; :: thesis: square-uparrow n c= [:NAT,NAT:] \ [:(Segm n),(Segm n):]
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in square-uparrow n or x in [:NAT,NAT:] \ [:(Segm n),(Segm n):] )
assume A1: x in square-uparrow n ; :: thesis: x in [:NAT,NAT:] \ [:(Segm n),(Segm n):]
then reconsider y = x as Element of [:NAT,NAT:] ;
consider n1, n2 being Nat such that
A2: n1 = y `1 and
A3: n2 = y `2 and
A4: n <= n1 and
n <= n2 by A1, Def3;
not x in [:(Segm n),(Segm n):]
proof
assume x in [:(Segm n),(Segm n):] ; :: thesis: contradiction
then ex x1, x2 being object st
( x1 in Segm n & x2 in Segm n & x = [x1,x2] ) by ZFMISC_1:def 2;
then ( n1 <= n - 1 & n2 <= n - 1 ) by A2, A3, STIRL2_1:10;
then n <= n - 1 by A4, XXREAL_0:2;
then n - n <= (n - 1) - n by XREAL_1:9;
then 0 <= - 1 ;
hence contradiction ; :: thesis: verum
end;
hence x in [:NAT,NAT:] \ [:(Segm n),(Segm n):] by A1, XBOOLE_0:def 5; :: thesis: verum