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 Def4; :: 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 Def4;
hence f is with_max by A1, Th15; :: thesis: f is with_min
for f being RealMap of T st f is continuous holds
f is with_max by A2, Th15;
hence f is with_min by A1, Th14; :: thesis: verum