let r be Element of RAT+ ; :: thesis: for B being set st B in DEDEKIND_CUTS \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } & not r in B & B <> {} holds
ex s being Element of RAT+ st
( not s in B & s < r )
let B be set ; :: thesis: ( B in DEDEKIND_CUTS \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } & not r in B & B <> {} implies ex s being Element of RAT+ st
( not s in B & s < r ) )
assume that
A1: B in DEDEKIND_CUTS \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } and
A2: not r in B and
A3: B <> {} ; :: thesis: ex s being Element of RAT+ st
( not s in B & s < r )
A4: B in DEDEKIND_CUTS by A1, XBOOLE_0:def 5;
assume A5: for s being Element of RAT+ st not s in B holds
not s < r ; :: thesis: contradiction
A6: B = { s where s is Element of RAT+ : s < r }
proof
thus B c= { s where s is Element of RAT+ : s < r } :: according to XBOOLE_0:def 10 :: thesis: { s where s is Element of RAT+ : s < r } c= B
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in B or e in { s where s is Element of RAT+ : s < r } )
assume A7: e in B ; :: thesis: e in { s where s is Element of RAT+ : s < r }
reconsider B = B as Element of DEDEKIND_CUTS by A1, XBOOLE_0:def 5;
B c= RAT+ ;
then reconsider t = e as Element of RAT+ by A7;
not r <=' t by A2, A4, A7, Lm16;
hence e in { s where s is Element of RAT+ : s < r } ; :: thesis: verum
end;
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { s where s is Element of RAT+ : s < r } or e in B )
assume e in { s where s is Element of RAT+ : s < r } ; :: thesis: e in B
then ex s being Element of RAT+ st
( s = e & s < r ) ;
hence e in B by A5; :: thesis: verum
end;
r <> {} by A2, A3, A4, Lm17;
then B in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } by A6;
hence contradiction by A1, XBOOLE_0:def 5; :: thesis: verum