L[01] (0,1,0,1) = (id (Closed-Interval-TSpace (0,1))) * (id (Closed-Interval-TSpace (0,1))) by BORSUK_6:def 1, TREAL_1:10, TREAL_1:14;
hence L[01] (0,1,0,1) = id (Closed-Interval-TSpace (0,1)) by SYSREL:12; :: thesis: verum