let r be real number ; :: thesis: ( 0 <= r & r <= 1 implies ( 0 <= 1 - r & 1 - r <= 1 ) )
assume ( 0 <= r & r <= 1 ) ; :: thesis: ( 0 <= 1 - r & 1 - r <= 1 )
then ( 1 - 1 <= 1 - r & 1 - r <= 1 - 0 ) by XREAL_1:15;
hence ( 0 <= 1 - r & 1 - r <= 1 ) ; :: thesis: verum