:: deftheorem defines L[01] BORSUK_6:def 1 :
for a, b, c, d being Real holds L[01] (a,b,c,d) = (L[01] (((#) (c,d)),((c,d) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#))));