let A be Element of DEDEKIND_CUTS ; :: thesis: ( GLUED A = {} iff A = {} )
thus ( GLUED A = {} implies A = {} ) :: thesis: ( A = {} implies GLUED A = {} )
proof
assume A1: GLUED A = {} ; :: thesis: A = {}
per cases ( ex r being Element of RAT+ st
for s being Element of RAT+ holds
( s in A iff s < r ) or for r being Element of RAT+ holds
not for s being Element of RAT+ holds
( s in A iff s < r ) ) ;
suppose A2: ex r being Element of RAT+ st
for s being Element of RAT+ holds
( s in A iff s < r ) ; :: thesis: A = {}
assume A <> {} ; :: thesis: contradiction
then consider r being Element of RAT+ such that
A3: r in A by SUBSET_1:4;
ex r being Element of RAT+ st
( GLUED A = r & ( for s being Element of RAT+ holds
( s in A iff s < r ) ) ) by A2, Def4;
then r < {} by A1, A3;
hence contradiction by ARYTM_3:64; :: thesis: verum
end;
suppose for r being Element of RAT+ holds
not for s being Element of RAT+ holds
( s in A iff s < r ) ; :: thesis: A = {}
hence A = {} by A1, Def4; :: thesis: verum
end;
end;
end;
assume A4: A = {} ; :: thesis: GLUED A = {}
then for s being Element of RAT+ holds
( s in A iff s < {} ) by ARYTM_3:64;
then consider r being Element of RAT+ such that
A5: GLUED A = r and
A6: for s being Element of RAT+ holds
( s in A iff s < r ) by Def4;
assume A7: GLUED A <> {} ; :: thesis: contradiction
{} <=' r by ARYTM_3:64;
then {} < r by A5, A7, ARYTM_3:68;
hence contradiction by A4, A6; :: thesis: verum