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