let F be ext-real-membered set ; :: thesis: for f being ext-real number st f in F holds
f " in F ""
let f be ext-real number ; :: thesis: ( f in F implies f " in F "" )
f in ExtREAL by XXREAL_0:def 1;
hence ( f in F implies f " in F "" ) ; :: thesis: verum