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

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