let L be non empty Lattice-like Boolean well-complemented properly_defined ShefferOrthoLattStr ; :: thesis: L is satisfying_Sheffer_3
let x, y, z be Element of L; :: according to SHEFFER1:def 15 :: thesis: (x | (y | z)) | (x | (y | z)) = ((y | y) | x) | ((z | z) | x)
x *' ((y `) + (z `)) = ((y `) *' x) + ((z `) *' x) by ROBBINS1:30;
then ((x `) + ((y | z) `)) ` = ((y `) *' x) + ((z `) *' x) by Def12;
then (x | (y | z)) ` = ((y `) *' x) + ((z `) *' x) by Def12;
then (x | (y | z)) | (x | (y | z)) = ((y `) *' x) + ((z `) *' x) by Def12
.= ((y `) *' ((x `) `)) + ((z `) *' x) by ROBBINS1:3
.= ((y `) *' ((x `) `)) + ((z `) *' ((x `) `)) by ROBBINS1:3
.= ((y + (x `)) `) + ((z `) *' ((x `) `)) by Th1
.= ((y + (x `)) `) + ((z + (x `)) `) by Th1
.= (y + (x `)) | (z + (x `)) by Def12
.= (((y `) `) + (x `)) | (z + (x `)) by ROBBINS1:3
.= (((y `) `) + (x `)) | (((z `) `) + (x `)) by ROBBINS1:3
.= ((y `) | x) | (((z `) `) + (x `)) by Def12
.= ((y `) | x) | ((z `) | x) by Def12
.= ((y | y) | x) | ((z `) | x) by Def12
.= ((y | y) | x) | ((z | z) | x) by Def12 ;
hence (x | (y | z)) | (x | (y | z)) = ((y | y) | x) | ((z | z) | x) ; :: thesis: verum