theorem :: TREAL_1:10

L[01] (((#) (0,1)),((0,1) (#))) = id (Closed-Interval-TSpace (0,1))