let r be real number ; :: thesis: ( 0 <= r & r <= 1 implies ( 0 <= 1 - r & 1 - r <= 1 ) )
assume that
A1: 0 <= r and
A2: r <= 1 ; :: thesis: ( 0 <= 1 - r & 1 - r <= 1 )
A3: 1 - 1 <= 1 - r by A2, XREAL_1:13;
1 - r <= 1 - 0 by A1, XREAL_1:13;
hence ( 0 <= 1 - r & 1 - r <= 1 ) by A3; :: thesis: verum