let f be RealMap of T; :: thesis: ( f is continuous implies ( f is bounded & f is with_max & f is with_min ) )
assume A1: f is continuous ; :: thesis: ( f is bounded & f is with_max & f is with_min )
hence f is bounded by Def27; :: thesis: ( f is with_max & f is with_min )
A2: for f being RealMap of T st f is continuous holds
f is bounded by Def27;
then A3: for f being RealMap of T st f is continuous holds
f is with_max by Th61;
thus f is with_max by A1, A2, Th61; :: thesis: f is with_min
thus f is with_min by A1, A3, Th60; :: thesis: verum