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