let L be non empty Lattice-like Boolean well-complemented properly_defined ShefferOrthoLattStr ; :: thesis: L is satisfying_Sheffer_1
let x be Element of L; :: according to SHEFFER1:def 13 :: thesis: (x | x) | (x | x) = x
(x `) ` = x by ROBBINS1:3;
then (x | x) ` = x by Def12;
hence (x | x) | (x | x) = x by Def12; :: thesis: verum