let E be Element of F; :: thesis: E is with_evenly_repeated_values

per cases ( F = {} or F <> {} ) ;

suppose F = {} ; :: thesis: E is with_evenly_repeated_values

hence E is with_evenly_repeated_values by SUBSET_1:def 1; :: thesis: verum

end;

suppose F <> {} ; :: thesis: E is with_evenly_repeated_values

hence E is with_evenly_repeated_values by Def7; :: thesis: verum

end;

end;