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

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