let a be positive light Real; :: thesis: ( max (a,(1 - a)) >= 1 / 2 & min (a,(1 - a)) <= 1 / 2 )

per cases ( a >= 1 - a or a < 1 - a ) ;

suppose B1: a >= 1 - a ; :: thesis: ( max (a,(1 - a)) >= 1 / 2 & min (a,(1 - a)) <= 1 / 2 )

then ( a + a >= (1 - a) + a & a + (1 - a) >= (1 - a) + (1 - a) ) by XREAL_1:6;
then ( (2 * a) / 2 >= 1 / 2 & (2 * (1 - a)) / 2 <= 1 / 2 ) by XREAL_1:72;
hence ( max (a,(1 - a)) >= 1 / 2 & min (a,(1 - a)) <= 1 / 2 ) by B1, XXREAL_0:def 9, XXREAL_0:def 10; :: thesis: verum

end;

suppose B1: a < 1 - a ; :: thesis: ( max (a,(1 - a)) >= 1 / 2 & min (a,(1 - a)) <= 1 / 2 )

then ( a + a < (1 - a) + a & a + (1 - a) < (1 - a) + (1 - a) ) by XREAL_1:6;
then ( (2 * a) / 2 < 1 / 2 & (2 * (1 - a)) / 2 > 1 / 2 ) by XREAL_1:74;
hence ( max (a,(1 - a)) >= 1 / 2 & min (a,(1 - a)) <= 1 / 2 ) by B1, XXREAL_0:def 9, XXREAL_0:def 10; :: thesis: verum

end;

end;