let F be ext-real-membered set ; :: thesis: for f being ExtReal st f in F holds
f " in F ""
let f be ExtReal; :: 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