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