let n be Nat; square-downarrow n = [:(Segm n),(Segm n):]
thus
square-downarrow n c= [:(Segm n),(Segm n):]
XBOOLE_0:def 10 [:(Segm n),(Segm n):] c= square-downarrow nproof
let x be
object ;
TARSKI:def 3 ( not x in square-downarrow n or x in [:(Segm n),(Segm n):] )
assume A2:
x in square-downarrow n
;
x in [:(Segm n),(Segm n):]
then consider n1,
n2 being
Nat such that A3:
n1 = x `1
and A4:
n2 = x `2
and A5:
n1 < n
and A6:
n2 < n
by Def4;
A7:
n1 in Segm n
by A5, NAT_1:44;
A8:
n2 in Segm n
by A6, NAT_1:44;
ex
x1,
x2 being
object st
(
x1 in NAT &
x2 in NAT &
x = [x1,x2] )
by A2, ZFMISC_1:def 2;
then reconsider x =
x as
pair object ;
x = [n1,n2]
by A3, A4;
hence
x in [:(Segm n),(Segm n):]
by A7, A8, ZFMISC_1:def 2;
verum
end;
let x be object ; TARSKI:def 3 ( not x in [:(Segm n),(Segm n):] or x in square-downarrow n )
assume
x in [:(Segm n),(Segm n):]
; x in square-downarrow n
then consider y1, y2 being object such that
A9:
y1 in Segm n
and
A10:
y2 in Segm n
and
A11:
x = [y1,y2]
by ZFMISC_1:def 2;
reconsider y1 = y1, y2 = y2 as Nat by A9, A10;
A12:
( y1 = x `1 & y2 = x `2 & y1 < n & y2 < n )
by A11, A9, A10, NAT_1:44;
x is Element of [:NAT,NAT:]
by A9, A10, A11, ZFMISC_1:def 2;
hence
x in square-downarrow n
by A12, Def4; verum