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

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