let A, B, C be Element of DEDEKIND_CUTS ; :: thesis: A *' (B *' C) c= (A *' B) *' C
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in A *' (B *' C) or e in (A *' B) *' C )
assume e in A *' (B *' C) ; :: thesis: e in (A *' B) *' C
then consider r0, s0 being Element of RAT+ such that
A1: ( e = r0 *' s0 & r0 in A ) and
A2: s0 in B *' C ;
consider r1, s1 being Element of RAT+ such that
A3: ( s0 = r1 *' s1 & r1 in B ) and
A4: s1 in C by A2;
( e = (r0 *' r1) *' s1 & r0 *' r1 in A *' B ) by A1, A3, ARYTM_3:52;
hence e in (A *' B) *' C by A4; :: thesis: verum