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

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