set Y = { z where z is Element of REAL : P2[z] } ;
set X = { z where z is Element of REAL : P1[z] } ;
A2: { z where z is Element of REAL : P1[z] } c= REAL
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { z where z is Element of REAL : P1[z] } or x in REAL )
assume x in { z where z is Element of REAL : P1[z] } ; :: thesis: x in REAL
then ex z being Element of REAL st
( z = x & P1[z] ) ;
hence x in REAL ; :: thesis: verum
end;
{ z where z is Element of REAL : P2[z] } c= REAL
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { z where z is Element of REAL : P2[z] } or x in REAL )
assume x in { z where z is Element of REAL : P2[z] } ; :: thesis: x in REAL
then ex z being Element of REAL st
( z = x & P2[z] ) ;
hence x in REAL ; :: thesis: verum
end;
then reconsider X = { z where z is Element of REAL : P1[z] } , Y = { z where z is Element of REAL : P2[z] } as Subset of REAL by A2;
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 that
A3: x in X and
A4: y in Y ; :: thesis: x <= y
A5: ex z being Element of REAL st
( z = y & P2[z] ) by A4;
ex z being Element of REAL st
( z = x & P1[z] ) by A3;
hence x <= y by A1, A5; :: thesis: verum
end;
then consider z being Real such that
A6: for x, y being Real st x in X & y in Y holds
( x <= z & z <= y ) by AXIOMS:1;
take z ; :: thesis: for x, y being Real st P1[x] & P2[y] holds
( x <= z & z <= y )
let x, y be Real; :: thesis: ( P1[x] & P2[y] implies ( x <= z & z <= y ) )
assume that
A7: P1[x] and
A8: P2[y] ; :: thesis: ( x <= z & z <= y )
y is Element of REAL by XREAL_0:def 1;
then A9: y in Y by A8;
x is Element of REAL by XREAL_0:def 1;
then x in X by A7;
hence ( x <= z & z <= y ) by A6, A9; :: thesis: verum