let x, y, z be Element of REAL+ ; :: thesis: x + (y + z) = (x + y) + z

per cases ( x = {} or y = {} or z = {} or ( x <> {} & y <> {} & z <> {} ) ) ;

suppose A1: x = {} ; :: thesis: x + (y + z) = (x + y) + z

hence x + (y + z) = y + z by Def8
.= (x + y) + z by A1, Def8 ;
:: thesis: verum

end;

suppose A2: y = {} ; :: thesis: x + (y + z) = (x + y) + z

hence x + (y + z) = x + z by Def8
.= (x + y) + z by A2, Def8 ;
:: thesis: verum

end;

suppose A3: z = {} ; :: thesis: x + (y + z) = (x + y) + z

hence x + (y + z) = x + y by Def8
.= (x + y) + z by A3, Def8 ;
:: thesis: verum

end;

suppose that A4: x <> {} and
A5: y <> {} and
A6: z <> {} ; :: thesis: x + (y + z) = (x + y) + z

A7: now :: thesis: not GLUED ((DEDEKIND_CUT y) + (DEDEKIND_CUT z)) = {}

assume GLUED ((DEDEKIND_CUT y) + (DEDEKIND_CUT z)) = {} ; :: thesis: contradiction
then (DEDEKIND_CUT y) + (DEDEKIND_CUT z) = {} by Lm11;
then ( DEDEKIND_CUT y = {} or DEDEKIND_CUT z = {} ) by Lm27;
hence contradiction by A5, A6, Lm10; :: thesis: verum

end;

A8: now :: thesis: not GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y)) = {}

assume GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y)) = {} ; :: thesis: contradiction
then (DEDEKIND_CUT x) + (DEDEKIND_CUT y) = {} by Lm11;
then ( DEDEKIND_CUT x = {} or DEDEKIND_CUT y = {} ) by Lm27;
hence contradiction by A4, A5, Lm10; :: thesis: verum

end;

thus x + (y + z) = x + (GLUED ((DEDEKIND_CUT y) + (DEDEKIND_CUT z))) by A5, A6, Def8
.= GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT (GLUED ((DEDEKIND_CUT y) + (DEDEKIND_CUT z))))) by A4, A7, Def8
.= GLUED ((DEDEKIND_CUT x) + ((DEDEKIND_CUT y) + (DEDEKIND_CUT z))) by Lm12
.= GLUED (((DEDEKIND_CUT x) + (DEDEKIND_CUT y)) + (DEDEKIND_CUT z)) by Lm26
.= GLUED ((DEDEKIND_CUT (GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y)))) + (DEDEKIND_CUT z)) by Lm12
.= (GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y))) + z by A6, A8, Def8
.= (x + y) + z by A4, A5, Def8 ; :: thesis: verum

end;

end;