:: deftheorem Def9 defines UpperUnitTriangle BORSUK_6:def 9 :
for b₁ being Subset of [:I[01],I[01]:] holds
( b₁ = UpperUnitTriangle iff for x being set holds
( x in b₁ iff ex a, b being Point of I[01] st
( x = [a,b] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) ) );