let A, B be non empty Subset of ExtREAL ; :: thesis: ( ( for r, s being R_eal st r in A & s in B holds
r <= s ) implies sup A <= inf B )
assume A1: for r, s being R_eal 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 R_eal such that
A2: ( s1 in A & inf B < s1 ) by Th8;
consider s2 being R_eal such that
A3: ( s2 in B & s2 < s1 ) by A2, Th9;
thus contradiction by A1, A2, A3; :: thesis: verum