let L be B_Lattice; :: thesis: for X, Y, Z being Element of L holds (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z)
let X, Y, Z be Element of L; :: thesis: (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z)
set S1 = X \ (Y "\/" Z);
set S2 = Y \ (X "\/" Z);
set S3 = Z \ (X "\/" Y);
set S4 = (X "/\" Y) "/\" Z;
thus (X \+\ Y) \+\ Z = (((X \ Y) \ Z) "\/" ((Y \ X) \ Z)) "\/" (Z \ ((X \ Y) "\/" (Y \ X))) by LATTICES:def 11
.= ((X \ (Y "\/" Z)) "\/" ((Y \ X) \ Z)) "\/" (Z \ ((X \ Y) "\/" (Y \ X))) by Th45
.= ((X \ (Y "\/" Z)) "\/" (Y \ (X "\/" Z))) "\/" (Z \ ((X \ Y) "\/" (Y \ X))) by Th45
.= ((X \ (Y "\/" Z)) "\/" (Y \ (X "\/" Z))) "\/" (Z \ ((X "\/" Y) \ (X "/\" Y))) by Th44
.= ((X \ (Y "\/" Z)) "\/" (Y \ (X "\/" Z))) "\/" ((Z \ (X "\/" Y)) "\/" ((X "/\" Y) "/\" Z)) by Th37
.= (((X \ (Y "\/" Z)) "\/" (Y \ (X "\/" Z))) "\/" ((X "/\" Y) "/\" Z)) "\/" (Z \ (X "\/" Y)) by LATTICES:def 5
.= (((X \ (Y "\/" Z)) "\/" ((X "/\" Y) "/\" Z)) "\/" (Y \ (X "\/" Z))) "\/" (Z \ (X "\/" Y)) by LATTICES:def 5
.= ((X \ (Y "\/" Z)) "\/" ((X "/\" Y) "/\" Z)) "\/" ((Y \ (X "\/" Z)) "\/" (Z \ (X "\/" Y))) by LATTICES:def 5
.= ((X \ (Y "\/" Z)) "\/" (X "/\" (Y "/\" Z))) "\/" ((Y \ (X "\/" Z)) "\/" (Z \ (X "\/" Y))) by LATTICES:def 7
.= (X \ ((Y "\/" Z) \ (Y "/\" Z))) "\/" ((Y \ (X "\/" Z)) "\/" (Z \ (X "\/" Y))) by Th37
.= (X \ ((Y \ Z) "\/" (Z \ Y))) "\/" ((Y \ (X "\/" Z)) "\/" (Z \ (X "\/" Y))) by Th44
.= (X \ ((Y \ Z) "\/" (Z \ Y))) "\/" ((Y \ (X "\/" Z)) "\/" ((Z \ Y) \ X)) by Th45
.= (X \ ((Y \ Z) "\/" (Z \ Y))) "\/" (((Y \ Z) \ X) "\/" ((Z \ Y) \ X)) by Th45
.= X \+\ (Y \+\ Z) by LATTICES:def 11 ; :: thesis: verum