let r be Real; :: 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 Lm1;

then ( 0 <= 1 - r & 1 - r <= 1 ) by Lm4;

hence 1 - r in the carrier of I[01] by Lm1; :: thesis: verum

assume r in the carrier of I[01] ; :: thesis: 1 - r in the carrier of I[01]

then ( 0 <= r & r <= 1 ) by Lm1;

then ( 0 <= 1 - r & 1 - r <= 1 ) by Lm4;

hence 1 - r in the carrier of I[01] by Lm1; :: thesis: verum