let A, B be Element of DEDEKIND_CUTS ; :: thesis: ( A = { r where r is Element of RAT+ : r < one } implies A *' B = B )
assume A1: A = { r where r is Element of RAT+ : r < one } ; :: thesis: A *' B = B
thus A *' B c= B :: according to XBOOLE_0:def 10 :: thesis: B c= A *' B
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in A *' B or e in B )
assume e in A *' B ; :: thesis: e in B
then consider r, s being Element of RAT+ such that
A2: e = r *' s and
A3: r in A and
A4: s in B ;
ex t being Element of RAT+ st
( t = r & t < one ) by A1, A3;
then r *' s <=' one *' s by ARYTM_3:82;
then r *' s <=' s by ARYTM_3:53;
hence e in B by A2, A4, Lm16; :: thesis: verum
end;
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in B or e in A *' B )
assume A5: e in B ; :: thesis: e in A *' B
then reconsider s = e as Element of RAT+ ;
consider s1 being Element of RAT+ such that
A6: s1 in B and
A7: s < s1 by A5, Lm7;
s1 <> {} by A7, ARYTM_3:64;
then consider s2 being Element of RAT+ such that
A8: s1 *' s2 = s by ARYTM_3:55;
A9: now :: thesis: not s2 = one
assume s2 = one ; :: thesis: contradiction
then s = s1 by A8, ARYTM_3:53;
hence contradiction by A7; :: thesis: verum
end;
one *' s = s2 *' s1 by A8, ARYTM_3:53;
then s2 <=' one by A7, ARYTM_3:83;
then s2 < one by A9, ARYTM_3:68;
then s2 in A by A1;
hence e in A *' B by A6, A8; :: thesis: verum