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:31;
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