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 SHEFFER1:def 5 :: thesis: x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z)
set X = x | x;
x "\/" (y "/\" z) = x "\/" ((y | z) | (y | z)) by Def12
.= (x | x) | (((y | z) ") ") by Def12
.= (x | x) | (y | z) by Def13
.= (((x | x) | (y | z)) ") " by Def13
.= (((y ") | (x | x)) | ((z ") | (x | x))) " by Def15
.= (((x | x) | (y ")) | ((z ") | (x | x))) " by Th31
.= (((x | x) | (y | y)) | ((x | x) | (z "))) " by Th31
.= ((x "\/" y) | ((x | x) | (z | z))) | (((x | x) | (y | y)) | ((x | x) | (z | z))) by Def12
.= ((x "\/" y) | (x "\/" z)) | (((x | x) | (y | y)) | ((x | x) | (z | z))) by Def12
.= ((x "\/" y) | (x "\/" z)) | ((x "\/" y) | ((x | x) | (z | z))) by Def12
.= ((x "\/" y) | (x "\/" z)) | ((x "\/" y) | (x "\/" z)) by Def12
.= (x "\/" y) "/\" (x "\/" z) by Def12 ;
hence x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z) ; :: thesis: verum