let X, Y be ext-real-membered set ; :: thesis: ( X c= Y implies inf Y <= inf X )
assume A1: X c= Y ; :: thesis: inf Y <= inf X
inf Y is LowerBound of Y by Def4;
then inf Y is LowerBound of X by A1, Th5;
hence inf Y <= inf X by Def4; :: thesis: verum