let z be Real; :: thesis: ( z in [.0,1.] & z <> 1 implies ex w being Element of [.0,1.] st w > z )
assume A1: ( z in [.0,1.] & z <> 1 ) ; :: thesis: ex w being Element of [.0,1.] st w > z
reconsider w = 1 as Element of [.0,1.] by XXREAL_1:1;
take w ; :: thesis: w > z
1 >= z by A1, XXREAL_1:1;
hence w > z by A1, XXREAL_0:1; :: thesis: verum