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

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