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;
hence DEDEKIND_CUT (GLUED A) = A by A9, Def3; :: thesis: verum
end;
end;