theorem :: TREAL_1:14

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