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