let A, B be non empty Subset of ExtREAL; :: thesis: ( ( for r, s being ExtReal st r in A & s in B holds
r <= s ) implies sup A <= inf B )
assume A1: for r, s being ExtReal st r in A & s in B holds
r <= s ; :: thesis: sup A <= inf B
assume not sup A <= inf B ; :: thesis: contradiction
then consider s1 being Element of ExtREAL such that
A2: s1 in A and
A3: inf B < s1 by Th94;
ex s2 being Element of ExtREAL st
( s2 in B & s2 < s1 ) by A3, Th95;
hence contradiction by A1, A2; :: thesis: verum