let a, b, c be set ; :: thesis: ( a c= c & b c= c \ a implies c = (a \/ (c \ (a \/ b))) \/ b )
assume that
A1: a c= c and
A2: b c= c \ a ; :: thesis: c = (a \/ (c \ (a \/ b))) \/ b
thus (a \/ (c \ (a \/ b))) \/ b = (a \/ ((c \ a) \ b)) \/ b by XBOOLE_1:41
.= a \/ (((c \ a) \ b) \/ b) by XBOOLE_1:4
.= a \/ ((c \ a) \/ b) by XBOOLE_1:39
.= a \/ (c \ a) by A2, XBOOLE_1:12
.= a \/ c by XBOOLE_1:39
.= c by A1, XBOOLE_1:12 ; :: thesis: verum