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:14;
then (x ` ) + (((y ` ) ` ) *' (y ` )) = x ` by ROBBINS1:16;
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