let r be Real; :: thesis: ( r in the carrier of I[01] implies 1 - r in the carrier of I[01] )
assume A1: r in the carrier of I[01] ; :: thesis: 1 - r in the carrier of I[01]
then A2: 0 <= r by BORSUK_1:43;
A3: r <= 1 by A1, BORSUK_1:43;
then A4: 0 <= 1 - r by A2, Lm1;
1 - r <= 1 by A2, A3, Lm1;
hence 1 - r in the carrier of I[01] by A4, BORSUK_1:43; :: thesis: verum