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