set A = { a where a is Element of ExtREAL : P₁[a] } ;
set B = { a where a is Element of ExtREAL : P₂[a] } ;
reconsider X = { a where a is Element of ExtREAL : P₁[a] } /\ REAL, Y = { a where a is Element of ExtREAL : P₂[a] } /\ REAL as Subset of REAL by XBOOLE_1:17;

per cases ( X = {} or Y = {} or ( X <> {} & Y <> {} ) ) ;

suppose A2: X = {} ; :: thesis: ex s being ExtReal st
( ( for r being ExtReal st P₁[r] holds
r <= s ) & ( for r being ExtReal st P₂[r] holds
s <= r ) )

per cases ( +infty in { a where a is Element of ExtREAL : P₁[a] } or not +infty in { a where a is Element of ExtREAL : P₁[a] } ) ;

suppose A3: +infty in { a where a is Element of ExtREAL : P₁[a] } ; :: thesis: ex s being ExtReal st
( ( for r being ExtReal st P₁[r] holds
r <= s ) & ( for r being ExtReal st P₂[r] holds
s <= r ) )

take +infty ; :: thesis: ( ( for r being ExtReal st P₁[r] holds
r <= +infty ) & ( for r being ExtReal st P₂[r] holds
+infty <= r ) )
thus for r being ExtReal st P₁[r] holds
r <= +infty by XXREAL_0:3; :: thesis: for r being ExtReal st P₂[r] holds
+infty <= r
ex a being Element of ExtREAL st
( a = +infty & P₁[a] ) by A3;
hence for r being ExtReal st P₂[r] holds
+infty <= r by A1; :: thesis: verum

end;

suppose A4: not +infty in { a where a is Element of ExtREAL : P₁[a] } ; :: thesis: ex s being ExtReal st
( ( for r being ExtReal st P₁[r] holds
r <= s ) & ( for r being ExtReal st P₂[r] holds
s <= r ) )

take -infty ; :: thesis: ( ( for r being ExtReal st P₁[r] holds
r <= -infty ) & ( for r being ExtReal st P₂[r] holds
-infty <= r ) )
thus for r being ExtReal st P₁[r] holds
r <= -infty :: thesis: for r being ExtReal st P₂[r] holds
-infty <= r

proof

let r be ExtReal; :: thesis: ( P₁[r] implies r <= -infty )
assume A5: P₁[r] ; :: thesis: r <= -infty
r in ExtREAL by XXREAL_0:def 1;
then A6: r in { a where a is Element of ExtREAL : P₁[a] } by A5;

per cases ( r = -infty or r in REAL ) by A4, A6, XXREAL_0:14;

suppose r = -infty ; :: thesis: r <= -infty

hence r <= -infty ; :: thesis: verum

end;

suppose r in REAL ; :: thesis: r <= -infty

hence r <= -infty by A2, A6, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

thus for r being ExtReal st P₂[r] holds
-infty <= r by XXREAL_0:5; :: thesis: verum

end;

end;

end;

suppose A7: Y = {} ; :: thesis: ex s being ExtReal st
( ( for r being ExtReal st P₁[r] holds
r <= s ) & ( for r being ExtReal st P₂[r] holds
s <= r ) )

per cases ( -infty in { a where a is Element of ExtREAL : P₂[a] } or not -infty in { a where a is Element of ExtREAL : P₂[a] } ) ;

suppose A8: -infty in { a where a is Element of ExtREAL : P₂[a] } ; :: thesis: ex s being ExtReal st
( ( for r being ExtReal st P₁[r] holds
r <= s ) & ( for r being ExtReal st P₂[r] holds
s <= r ) )

take -infty ; :: thesis: ( ( for r being ExtReal st P₁[r] holds
r <= -infty ) & ( for r being ExtReal st P₂[r] holds
-infty <= r ) )
ex a being Element of ExtREAL st
( a = -infty & P₂[a] ) by A8;
hence for r being ExtReal st P₁[r] holds
r <= -infty by A1; :: thesis: for r being ExtReal st P₂[r] holds
-infty <= r
thus for r being ExtReal st P₂[r] holds
-infty <= r by XXREAL_0:5; :: thesis: verum

end;

suppose A9: not -infty in { a where a is Element of ExtREAL : P₂[a] } ; :: thesis: ex s being ExtReal st
( ( for r being ExtReal st P₁[r] holds
r <= s ) & ( for r being ExtReal st P₂[r] holds
s <= r ) )

take +infty ; :: thesis: ( ( for r being ExtReal st P₁[r] holds
r <= +infty ) & ( for r being ExtReal st P₂[r] holds
+infty <= r ) )
thus for r being ExtReal st P₁[r] holds
r <= +infty by XXREAL_0:3; :: thesis: for r being ExtReal st P₂[r] holds
+infty <= r
let r be ExtReal; :: thesis: ( P₂[r] implies +infty <= r )
assume A10: P₂[r] ; :: thesis: +infty <= r
r in ExtREAL by XXREAL_0:def 1;
then A11: r in { a where a is Element of ExtREAL : P₂[a] } by A10;

per cases ( r = +infty or r in REAL ) by A9, A11, XXREAL_0:14;

suppose r = +infty ; :: thesis: +infty <= r

hence +infty <= r ; :: thesis: verum

end;

suppose r in REAL ; :: thesis: +infty <= r

hence +infty <= r by A7, A11, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

end;

end;

suppose that A12: X <> {} and
A13: Y <> {} ; :: thesis: ex s being ExtReal st
( ( for r being ExtReal st P₁[r] holds
r <= s ) & ( for r being ExtReal st P₂[r] holds
s <= r ) )

for x, y being Real st x in X & y in Y holds
x <= y

proof

let x, y be Real; :: thesis: ( x in X & y in Y implies x <= y )
assume x in X ; :: thesis: ( not y in Y or x <= y )
then x in { a where a is Element of ExtREAL : P₁[a] } by XBOOLE_0:def 4;
then A14: ex a being Element of ExtREAL st
( a = x & P₁[a] ) ;
assume y in Y ; :: thesis: x <= y
then y in { a where a is Element of ExtREAL : P₂[a] } by XBOOLE_0:def 4;
then ex a being Element of ExtREAL st
( a = y & P₂[a] ) ;
hence x <= y by A1, A14; :: thesis: verum

end;

then consider s being Real such that
A15: for x, y being Real st x in X & y in Y holds
( x <= s & s <= y ) by AXIOMS:1;
reconsider s = s as ExtReal ;
take s ; :: thesis: ( ( for r being ExtReal st P₁[r] holds
r <= s ) & ( for r being ExtReal st P₂[r] holds
s <= r ) )
thus for r being ExtReal st P₁[r] holds
r <= s :: thesis: for r being ExtReal st P₂[r] holds
s <= r

proof

let r be ExtReal; :: thesis: ( P₁[r] implies r <= s )
consider x being Element of REAL such that
A16: x in Y by A13;
x in { a where a is Element of ExtREAL : P₂[a] } by A16, XBOOLE_0:def 4;
then A17: ex a being Element of ExtREAL st
( x = a & P₂[a] ) ;
assume A18: P₁[r] ; :: thesis: r <= s

per cases ( r in REAL or r = -infty ) by A1, A17, A18, XXREAL_0:13;

suppose A19: r in REAL ; :: thesis: r <= s

then reconsider r = r as Real ;
r is Element of ExtREAL by XXREAL_0:def 1;
then r in { a where a is Element of ExtREAL : P₁[a] } by A18;
then r in X by A19, XBOOLE_0:def 4;
hence r <= s by A15, A16; :: thesis: verum

end;

suppose r = -infty ; :: thesis: r <= s

hence r <= s by XXREAL_0:5; :: thesis: verum

end;

end;

end;

let r be ExtReal; :: thesis: ( P₂[r] implies s <= r )
consider x being Element of REAL such that
A20: x in X by A12;
x in { a where a is Element of ExtREAL : P₁[a] } by A20, XBOOLE_0:def 4;
then A21: ex a being Element of ExtREAL st
( x = a & P₁[a] ) ;
assume A22: P₂[r] ; :: thesis: s <= r

per cases ( r in REAL or r = +infty ) by A1, A21, A22, XXREAL_0:10;

suppose A23: r in REAL ; :: thesis: s <= r

then reconsider r = r as Real ;
r is Element of ExtREAL by XXREAL_0:def 1;
then r in { a where a is Element of ExtREAL : P₂[a] } by A22;
then r in Y by A23, XBOOLE_0:def 4;
hence s <= r by A15, A20; :: thesis: verum

end;

suppose r = +infty ; :: thesis: s <= r

hence s <= r by XXREAL_0:3; :: thesis: verum

end;

end;

end;

end;