:: deftheorem Def3 defines square-uparrow CARDFIL4:def 4 :
for n being Nat
for b₂ being Subset of [:NAT,NAT:] holds
( b₂ = square-uparrow 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 & n <= n1 & n <= n2 ) ) );