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

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