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

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