set Y = { z where z is Element of REAL : P_{2}[z] } ;

set X = { z where z is Element of REAL : P_{1}[z] } ;

A2: { z where z is Element of REAL : P_{1}[z] } c= REAL
_{2}[z] } c= REAL
_{1}[z] } , Y = { z where z is Element of REAL : P_{2}[z] } as Subset of REAL by A2;

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

x <= y

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 P_{1}[x] & P_{2}[y] holds

( x <= z & z <= y )

let x, y be Real; :: thesis: ( P_{1}[x] & P_{2}[y] implies ( x <= z & z <= y ) )

assume that

A7: P_{1}[x]
and

A8: P_{2}[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

set X = { z where z is Element of REAL : P

A2: { z where z is Element of REAL : P

proof

{ z where z is Element of REAL : P
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { z where z is Element of REAL : P_{1}[z] } or x in REAL )

assume x in { z where z is Element of REAL : P_{1}[z] }
; :: thesis: x in REAL

then ex z being Element of REAL st

( z = x & P_{1}[z] )
;

hence x in REAL ; :: thesis: verum

end;assume x in { z where z is Element of REAL : P

then ex z being Element of REAL st

( z = x & P

hence x in REAL ; :: thesis: verum

proof

then reconsider X = { z where z is Element of REAL : P
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { z where z is Element of REAL : P_{2}[z] } or x in REAL )

assume x in { z where z is Element of REAL : P_{2}[z] }
; :: thesis: x in REAL

then ex z being Element of REAL st

( z = x & P_{2}[z] )
;

hence x in REAL ; :: thesis: verum

end;assume x in { z where z is Element of REAL : P

then ex z being Element of REAL st

( z = x & P

hence x in REAL ; :: thesis: verum

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

x <= y

proof

then consider z being Real such that
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 & P_{2}[z] )
by A4;

ex z being Element of REAL st

( z = x & P_{1}[z] )
by A3;

hence x <= y by A1, A5; :: thesis: verum

end;assume that

A3: x in X and

A4: y in Y ; :: thesis: x <= y

A5: ex z being Element of REAL st

( z = y & P

ex z being Element of REAL st

( z = x & P

hence x <= y by A1, A5; :: thesis: verum

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 P

( x <= z & z <= y )

let x, y be Real; :: thesis: ( P

assume that

A7: P

A8: P

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