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;