let L be non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr ; :: thesis: L is distributive

let x, y, z be Element of L; :: according to LATTICES:def 11 :: thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)

set Y = y " ;

set Z = z " ;

x "/\" (y "\/" z) = x "/\" ((y | y) | (z | z)) by Def12

.= (x | ((y ") | (z "))) " by Def12

.= (((y ") ") | x) | (((z ") ") | x) by Def15

.= (y | x) | (((z ") ") | x) by Def13

.= (y | x) | (z | x) by Def13

.= (x | y) | (z | x) by Th31

.= (x | y) | (x | z) by Th31

.= (((x | y) ") ") | (x | z) by Def13

.= (((x | y) | (x | y)) ") | (((x | z) ") ") by Def13

.= ((x "/\" y) | ((x | y) | (x | y))) | (((x | z) | (x | z)) | ((x | z) | (x | z))) by Def12

.= ((x "/\" y) | (x "/\" y)) | (((x | z) | (x | z)) | ((x | z) | (x | z))) by Def12

.= ((x "/\" y) | (x "/\" y)) | ((x "/\" z) | ((x | z) | (x | z))) by Def12

.= ((x "/\" y) | (x "/\" y)) | ((x "/\" z) | (x "/\" z)) by Def12

.= (x "/\" y) "\/" (x "/\" z) by Def12 ;

hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) ; :: thesis: verum

let x, y, z be Element of L; :: according to LATTICES:def 11 :: thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)

set Y = y " ;

set Z = z " ;

x "/\" (y "\/" z) = x "/\" ((y | y) | (z | z)) by Def12

.= (x | ((y ") | (z "))) " by Def12

.= (((y ") ") | x) | (((z ") ") | x) by Def15

.= (y | x) | (((z ") ") | x) by Def13

.= (y | x) | (z | x) by Def13

.= (x | y) | (z | x) by Th31

.= (x | y) | (x | z) by Th31

.= (((x | y) ") ") | (x | z) by Def13

.= (((x | y) | (x | y)) ") | (((x | z) ") ") by Def13

.= ((x "/\" y) | ((x | y) | (x | y))) | (((x | z) | (x | z)) | ((x | z) | (x | z))) by Def12

.= ((x "/\" y) | (x "/\" y)) | (((x | z) | (x | z)) | ((x | z) | (x | z))) by Def12

.= ((x "/\" y) | (x "/\" y)) | ((x "/\" z) | ((x | z) | (x | z))) by Def12

.= ((x "/\" y) | (x "/\" y)) | ((x "/\" z) | (x "/\" z)) by Def12

.= (x "/\" y) "\/" (x "/\" z) by Def12 ;

hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) ; :: thesis: verum