let a, b be Element of [.0,1.]; :: thesis: ( max (a,b) <> 1 implies ( a <> 1 & b <> 1 ) )
assume A1: max (a,b) <> 1 ; :: thesis: ( a <> 1 & b <> 1 )
A2: ( a <= 1 & b <= 1 ) by XXREAL_1:1;
assume ( a = 1 or b = 1 ) ; :: thesis: contradiction

per cases then ( a = 1 or b = 1 ) ;

suppose a = 1 ; :: thesis: contradiction

hence contradiction by A1, A2, XXREAL_0:def 10; :: thesis: verum

end;

suppose b = 1 ; :: thesis: contradiction

hence contradiction by A1, A2, XXREAL_0:def 10; :: thesis: verum

end;

end;