:: deftheorem Def4 defines square-downarrow CARDFIL4:def 5 :
for n being Nat
for b₂ being Subset of [:NAT,NAT:] holds
( b₂ = square-downarrow n iff for x being Element of [:NAT,NAT:] holds
( x in b₂ iff ex n1, n2 being Nat st
( n1 = x `1 & n2 = x `2 & n1 < n & n2 < n ) ) );