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 Lm25;
hence A + (B + C) = (A + B) + C by XBOOLE_0:def 10; :: thesis: verum