let A, B, C be Element of DEDEKIND_CUTS ; :: thesis: A *' (B *' C) = (A *' B) *' C
( A *' (B *' C) c= (A *' B) *' C & (A *' B) *' C c= A *' (B *' C) ) by Lm38;
hence A *' (B *' C) = (A *' B) *' C by XBOOLE_0:def 10; :: thesis: verum