:: deftheorem Def8 defines LowerLeftUnitTriangle BORSUK_6:def 8 :
for b₁ being Subset of [:I[01],I[01]:] holds
( b₁ = LowerLeftUnitTriangle 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) ) ) );