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