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 Th32
.= (x | y) | (x | z) by Th32
.= (((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