let r be real number ; :: thesis: ( r in the carrier of I[01] implies 1 - r in the carrier of I[01] )
assume r in the carrier of I[01] ; :: thesis: 1 - r in the carrier of I[01]
then ( 0 <= r & r <= 1 ) by BORSUK_1:86;
then ( 0 <= 1 - r & 1 - r <= 1 ) by Lm1;
hence 1 - r in the carrier of I[01] by BORSUK_1:86; :: thesis: verum