let A be Element of DEDEKIND_CUTS ; :: thesis: DEDEKIND_CUT (GLUED A) = A

per cases ( ex r being Element of RAT+ st
for s being Element of RAT+ holds
( s in A iff s < r ) or A = {} or ( A <> {} & ( for r being Element of RAT+ holds
not for s being Element of RAT+ holds
( s in A iff s < r ) ) ) ) ;

suppose ex r being Element of RAT+ st
for s being Element of RAT+ holds
( s in A iff s < r ) ; :: thesis: DEDEKIND_CUT (GLUED A) = A

then consider r being Element of RAT+ such that
A1: r = GLUED A and
A2: for s being Element of RAT+ holds
( s in A iff s < r ) by Def4;
consider s being Element of RAT+ such that
A3: r = s and
A4: DEDEKIND_CUT (GLUED A) = { t where t is Element of RAT+ : t < s } by A1, Def3;
thus DEDEKIND_CUT (GLUED A) c= A :: according to XBOOLE_0:def 10 :: thesis: A c= DEDEKIND_CUT (GLUED A)

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in DEDEKIND_CUT (GLUED A) or e in A )
assume e in DEDEKIND_CUT (GLUED A) ; :: thesis: e in A
then ex t being Element of RAT+ st
( t = e & t < s ) by A4;
hence e in A by A2, A3; :: thesis: verum

end;

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in A or e in DEDEKIND_CUT (GLUED A) )
assume A5: e in A ; :: thesis: e in DEDEKIND_CUT (GLUED A)
then reconsider s = e as Element of RAT+ ;
s < r by A2, A5;
hence e in DEDEKIND_CUT (GLUED A) by A3, A4; :: thesis: verum

end;

suppose A6: A = {} ; :: thesis: DEDEKIND_CUT (GLUED A) = A

then GLUED A = {} by Lm11;
hence DEDEKIND_CUT (GLUED A) = A by A6, Lm10; :: thesis: verum

end;

suppose that A7: A <> {} and
A8: for r being Element of RAT+ holds
not for s being Element of RAT+ holds
( s in A iff s < r ) ; :: thesis: DEDEKIND_CUT (GLUED A) = A

A9: GLUED A = A by A8, Def4;

now :: thesis: not GLUED A in RAT+

assume GLUED A in RAT+ ; :: thesis: contradiction
then GLUED A in RAT+ /\ DEDEKIND_CUTS by A9, XBOOLE_0:def 4;
then GLUED A = {} by Lm9, TARSKI:def 1;
hence contradiction by A7, Lm11; :: thesis: verum

end;

hence DEDEKIND_CUT (GLUED A) = A by A9, Def3; :: thesis: verum

end;

end;