:: SHEFFER1 semantic presentation

begin

theorem :: SHEFFER1:1
for L being ( ( non empty join-commutative join-associative Huntington ) ( non empty join-commutative join-associative upper-bounded Huntington join-idempotent ) ComplLLattStr )
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty join-commutative join-associative Huntington ) ( non empty join-commutative join-associative upper-bounded Huntington join-idempotent ) ComplLLattStr ) : ( ( ) ( non empty ) set ) )) ` : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty join-commutative join-associative Huntington ) ( non empty join-commutative join-associative upper-bounded Huntington join-idempotent ) ComplLLattStr ) : ( ( ) ( non empty ) set ) )) = (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty join-commutative join-associative Huntington ) ( non empty join-commutative join-associative upper-bounded Huntington join-idempotent ) ComplLLattStr ) : ( ( ) ( non empty ) set ) )) *' (b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty join-commutative join-associative Huntington ) ( non empty join-commutative join-associative upper-bounded Huntington join-idempotent ) ComplLLattStr ) : ( ( ) ( non empty ) set ) )) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty join-commutative join-associative Huntington ) ( non empty join-commutative join-associative upper-bounded Huntington join-idempotent ) ComplLLattStr ) : ( ( ) ( non empty ) set ) )) ;

begin

definition
let IT be ( ( non empty ) ( non empty ) LattStr ) ;
attr IT is upper-bounded' means :: SHEFFER1:def 1
 ex c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M2( the carrier of IT : ( ( ) ( ) OrthoLattStr ) : ( ( ) ( ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M2( the carrier of IT : ( ( ) ( ) OrthoLattStr ) : ( ( ) ( ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) );
end;

definition
let L be ( ( non empty ) ( non empty ) LattStr ) ;
assume L : ( ( non empty ) ( non empty ) LattStr ) is upper-bounded' ;
func Top' L -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) means :: SHEFFER1:def 2
 for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( it : ( ( V6() V18(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) ) ( V6() V18(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) ) M2(K19(K20(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) "/\" a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M2( the carrier of L : ( ( ) ( ) OrthoLattStr ) : ( ( ) ( ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" it : ( ( V6() V18(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) ) ( V6() V18(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) ) M2(K19(K20(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of L : ( ( ) ( ) OrthoLattStr ) : ( ( ) ( ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) );
end;

definition
let IT be ( ( non empty ) ( non empty ) LattStr ) ;
attr IT is lower-bounded' means :: SHEFFER1:def 3
 ex c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M2( the carrier of IT : ( ( ) ( ) OrthoLattStr ) : ( ( ) ( ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M2( the carrier of IT : ( ( ) ( ) OrthoLattStr ) : ( ( ) ( ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) );
end;

definition
let L be ( ( non empty ) ( non empty ) LattStr ) ;
assume L : ( ( non empty ) ( non empty ) LattStr ) is lower-bounded' ;
func Bot' L -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) means :: SHEFFER1:def 4
 for a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( it : ( ( V6() V18(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) ) ( V6() V18(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) ) M2(K19(K20(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) "\/" a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M2( the carrier of L : ( ( ) ( ) OrthoLattStr ) : ( ( ) ( ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" it : ( ( V6() V18(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) ) ( V6() V18(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) ) M2(K19(K20(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of L : ( ( ) ( ) OrthoLattStr ) : ( ( ) ( ) set ) )) = a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) );
end;

definition
let IT be ( ( non empty ) ( non empty ) LattStr ) ;
attr IT is distributive' means :: SHEFFER1:def 5
 for a, b, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" (b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of IT : ( ( ) ( ) OrthoLattStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of IT : ( ( ) ( ) OrthoLattStr ) : ( ( ) ( ) set ) )) = (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of IT : ( ( ) ( ) OrthoLattStr ) : ( ( ) ( ) set ) )) "/\" (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of IT : ( ( ) ( ) OrthoLattStr ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of IT : ( ( ) ( ) OrthoLattStr ) : ( ( ) ( ) set ) )) ;
end;

definition
let L be ( ( non empty ) ( non empty ) LattStr ) ;
let a, b be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
pred a is_a_complement'_of b means :: SHEFFER1:def 6
( b : ( ( V6() V18(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) ) ( V6() V18(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) ) M2(K19(K20(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) "\/" a : ( ( V6() V18(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) ) ( V6() V18(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) ) M2(K19(K20(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of L : ( ( ) ( ) OrthoLattStr ) : ( ( ) ( ) set ) )) = Top' L : ( ( ) ( ) OrthoLattStr ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & a : ( ( V6() V18(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) ) ( V6() V18(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) ) M2(K19(K20(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) "\/" b : ( ( V6() V18(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) ) ( V6() V18(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) ) M2(K19(K20(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of L : ( ( ) ( ) OrthoLattStr ) : ( ( ) ( ) set ) )) = Top' L : ( ( ) ( ) OrthoLattStr ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & b : ( ( V6() V18(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) ) ( V6() V18(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) ) M2(K19(K20(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) "/\" a : ( ( V6() V18(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) ) ( V6() V18(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) ) M2(K19(K20(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of L : ( ( ) ( ) OrthoLattStr ) : ( ( ) ( ) set ) )) = Bot' L : ( ( ) ( ) OrthoLattStr ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & a : ( ( V6() V18(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) ) ( V6() V18(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) ) M2(K19(K20(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) "/\" b : ( ( V6() V18(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) ) ( V6() V18(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) ) M2(K19(K20(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of L : ( ( ) ( ) OrthoLattStr ) : ( ( ) ( ) set ) )) = Bot' L : ( ( ) ( ) OrthoLattStr ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) );
end;

definition
let IT be ( ( non empty ) ( non empty ) LattStr ) ;
attr IT is complemented' means :: SHEFFER1:def 7
 for b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) ex a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is_a_complement'_of b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
end;

definition
let L be ( ( non empty ) ( non empty ) LattStr ) ;
let x be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
assume ( L : ( ( non empty ) ( non empty ) LattStr ) is complemented' & L : ( ( non empty ) ( non empty ) LattStr ) is distributive & L : ( ( non empty ) ( non empty ) LattStr ) is upper-bounded' & L : ( ( non empty ) ( non empty ) LattStr ) is meet-commutative ) ;
func x `# -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) means :: SHEFFER1:def 8
it : ( ( V6() V18(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) ) ( V6() V18(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) ) M2(K19(K20(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) is_a_complement'_of x : ( ( V6() V18(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) ) ( V6() V18(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) ) M2(K19(K20(K20(L : ( ( ) ( ) OrthoLattStr ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ,L : ( ( ) ( ) OrthoLattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ;
end;

registration
cluster non empty V45() V46() 1 : ( ( ) ( ) set ) -element Lattice-like Boolean join-idempotent upper-bounded' lower-bounded' distributive' complemented' for ( ( ) ( ) LattStr ) ;
end;

theorem :: SHEFFER1:2
for L being ( ( non empty join-commutative meet-commutative distributive upper-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive upper-bounded' distributive' complemented' ) LattStr )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) `#) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty join-commutative meet-commutative distributive upper-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive upper-bounded' distributive' complemented' ) LattStr ) : ( ( ) ( non empty ) set ) )) = Top' L : ( ( non empty join-commutative meet-commutative distributive upper-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive upper-bounded' distributive' complemented' ) LattStr ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: SHEFFER1:3
for L being ( ( non empty join-commutative meet-commutative distributive upper-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive upper-bounded' distributive' complemented' ) LattStr )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) `#) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty join-commutative meet-commutative distributive upper-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive upper-bounded' distributive' complemented' ) LattStr ) : ( ( ) ( non empty ) set ) )) = Bot' L : ( ( non empty join-commutative meet-commutative distributive upper-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive upper-bounded' distributive' complemented' ) LattStr ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: SHEFFER1:4
for L being ( ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' distributive' complemented' ) LattStr )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" (Top' L : ( ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' distributive' complemented' ) LattStr ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' distributive' complemented' ) LattStr ) : ( ( ) ( non empty ) set ) )) = Top' L : ( ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' distributive' complemented' ) LattStr ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: SHEFFER1:5
for L being ( ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) LattStr )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" (Bot' L : ( ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) LattStr ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) LattStr ) : ( ( ) ( non empty ) set ) )) = Bot' L : ( ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) LattStr ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: SHEFFER1:6
for L being ( ( non empty join-commutative meet-commutative meet-absorbing join-absorbing distributive join-idempotent ) ( non empty join-commutative meet-commutative meet-absorbing join-absorbing distributive join-idempotent ) LattStr )
for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds ((x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty join-commutative meet-commutative meet-absorbing join-absorbing distributive join-idempotent ) ( non empty join-commutative meet-commutative meet-absorbing join-absorbing distributive join-idempotent ) LattStr ) : ( ( ) ( non empty ) set ) )) "\/" z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty join-commutative meet-commutative meet-absorbing join-absorbing distributive join-idempotent ) ( non empty join-commutative meet-commutative meet-absorbing join-absorbing distributive join-idempotent ) LattStr ) : ( ( ) ( non empty ) set ) )) "/\" x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty join-commutative meet-commutative meet-absorbing join-absorbing distributive join-idempotent ) ( non empty join-commutative meet-commutative meet-absorbing join-absorbing distributive join-idempotent ) LattStr ) : ( ( ) ( non empty ) set ) )) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: SHEFFER1:7
for L being ( ( non empty join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent distributive' ) ( non empty join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent distributive' ) LattStr )
for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds ((x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent distributive' ) ( non empty join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent distributive' ) LattStr ) : ( ( ) ( non empty ) set ) )) "/\" z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent distributive' ) ( non empty join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent distributive' ) LattStr ) : ( ( ) ( non empty ) set ) )) "\/" x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent distributive' ) ( non empty join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent distributive' ) LattStr ) : ( ( ) ( non empty ) set ) )) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

definition
let G be ( ( non empty ) ( non empty ) /\-SemiLattStr ) ;
attr G is meet-idempotent means :: SHEFFER1:def 9
 for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M2( the carrier of G : ( ( ) ( ) OrthoLattStr ) : ( ( ) ( ) set ) )) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
end;

theorem :: SHEFFER1:8
for L being ( ( non empty join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' complemented' ) LattStr ) holds L : ( ( non empty join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' complemented' ) LattStr ) is meet-idempotent ;

theorem :: SHEFFER1:9
for L being ( ( non empty join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' complemented' ) LattStr ) holds L : ( ( non empty join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' complemented' ) LattStr ) is join-idempotent ;

theorem :: SHEFFER1:10
for L being ( ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' distributive' complemented' ) LattStr ) holds L : ( ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' distributive' complemented' ) LattStr ) is meet-absorbing ;

theorem :: SHEFFER1:11
for L being ( ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) LattStr ) holds L : ( ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) LattStr ) is join-absorbing ;

theorem :: SHEFFER1:12
for L being ( ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) LattStr ) holds L : ( ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) LattStr ) is upper-bounded ;

theorem :: SHEFFER1:13
for L being ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V68() complemented Boolean ) LattStr ) holds L : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V68() complemented Boolean ) LattStr ) is upper-bounded' ;

theorem :: SHEFFER1:14
for L being ( ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) LattStr ) holds L : ( ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) LattStr ) is lower-bounded ;

theorem :: SHEFFER1:15
for L being ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V68() complemented Boolean ) LattStr ) holds L : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V68() complemented Boolean ) LattStr ) is lower-bounded' ;

theorem :: SHEFFER1:16
for L being ( ( non empty join-commutative meet-commutative meet-absorbing join-absorbing distributive join-idempotent ) ( non empty join-commutative meet-commutative meet-absorbing join-absorbing distributive join-idempotent ) LattStr ) holds L : ( ( non empty join-commutative meet-commutative meet-absorbing join-absorbing distributive join-idempotent ) ( non empty join-commutative meet-commutative meet-absorbing join-absorbing distributive join-idempotent ) LattStr ) is join-associative ;

theorem :: SHEFFER1:17
for L being ( ( non empty join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent distributive' ) ( non empty join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent distributive' ) LattStr ) holds L : ( ( non empty join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent distributive' ) ( non empty join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent distributive' ) LattStr ) is meet-associative ;

theorem :: SHEFFER1:18
for L being ( ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) LattStr ) holds Top L : ( ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) LattStr ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) LattStr ) : ( ( ) ( non empty ) set ) )) = Top' L : ( ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) LattStr ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: SHEFFER1:19
for L being ( ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) LattStr ) holds Bottom L : ( ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) LattStr ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) LattStr ) : ( ( ) ( non empty ) set ) )) = Bot' L : ( ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) LattStr ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: SHEFFER1:20
for L being ( ( non empty Lattice-like Boolean distributive' ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V68() complemented Boolean distributive' ) LattStr ) holds Top L : ( ( non empty Lattice-like Boolean distributive' ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V68() complemented Boolean distributive' ) LattStr ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty Lattice-like Boolean distributive' ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V68() complemented Boolean distributive' ) LattStr ) : ( ( ) ( non empty ) set ) )) = Top' L : ( ( non empty Lattice-like Boolean distributive' ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V68() complemented Boolean distributive' ) LattStr ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: SHEFFER1:21
for L being ( ( non empty Lattice-like distributive lower-bounded upper-bounded complemented Boolean distributive' ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V68() complemented Boolean distributive' ) LattStr ) holds Bottom L : ( ( non empty Lattice-like distributive lower-bounded upper-bounded complemented Boolean distributive' ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V68() complemented Boolean distributive' ) LattStr ) : ( ( ) ( ) M2( the carrier of b1 : ( ( non empty Lattice-like distributive lower-bounded upper-bounded complemented Boolean distributive' ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V68() complemented Boolean distributive' ) LattStr ) : ( ( ) ( non empty ) set ) )) = Bot' L : ( ( non empty Lattice-like distributive lower-bounded upper-bounded complemented Boolean distributive' ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V68() complemented Boolean distributive' ) LattStr ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: SHEFFER1:22
for L being ( ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) LattStr )
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is_a_complement'_of y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) iff x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is_a_complement_of y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

theorem :: SHEFFER1:23
for L being ( ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) LattStr ) holds L : ( ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) ( non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' ) LattStr ) is complemented ;

theorem :: SHEFFER1:24
for L being ( ( non empty Lattice-like Boolean upper-bounded' lower-bounded' distributive' ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V68() complemented Boolean upper-bounded' lower-bounded' distributive' ) LattStr ) holds L : ( ( non empty Lattice-like Boolean upper-bounded' lower-bounded' distributive' ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V68() complemented Boolean upper-bounded' lower-bounded' distributive' ) LattStr ) is complemented' ;

theorem :: SHEFFER1:25
for L being ( ( non empty ) ( non empty ) LattStr ) holds
( L : ( ( non empty ) ( non empty ) LattStr ) is ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V68() complemented Boolean ) Lattice) iff ( L : ( ( non empty ) ( non empty ) LattStr ) is lower-bounded' & L : ( ( non empty ) ( non empty ) LattStr ) is upper-bounded' & L : ( ( non empty ) ( non empty ) LattStr ) is join-commutative & L : ( ( non empty ) ( non empty ) LattStr ) is meet-commutative & L : ( ( non empty ) ( non empty ) LattStr ) is distributive & L : ( ( non empty ) ( non empty ) LattStr ) is distributive' & L : ( ( non empty ) ( non empty ) LattStr ) is complemented' ) ) ;

registration
cluster non empty Lattice-like Boolean -> non empty join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' complemented' for ( ( ) ( ) LattStr ) ;
cluster non empty join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' complemented' -> non empty Lattice-like Boolean for ( ( ) ( ) LattStr ) ;
end;

begin

definition
attr c1 is strict ;
struct ShefferStr -> ( ( ) ( ) 1-sorted ) ;
aggr ShefferStr(# carrier, stroke #) -> ( ( strict ) ( strict ) ShefferStr ) ;
sel stroke c1 -> ( ( V6() V18(K20( the carrier of c1 : ( ( cardinal ) ( V26() cardinal ) set ) : ( ( ) ( ) set ) , the carrier of c1 : ( ( cardinal ) ( V26() cardinal ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) , the carrier of c1 : ( ( cardinal ) ( V26() cardinal ) set ) : ( ( ) ( ) set ) ) ) ( V6() V18(K20( the carrier of c1 : ( ( cardinal ) ( V26() cardinal ) set ) : ( ( ) ( ) set ) , the carrier of c1 : ( ( cardinal ) ( V26() cardinal ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) , the carrier of c1 : ( ( cardinal ) ( V26() cardinal ) set ) : ( ( ) ( ) set ) ) ) BinOp of the carrier of c1 : ( ( cardinal ) ( V26() cardinal ) set ) : ( ( ) ( ) set ) ) ;
end;

definition
attr c1 is strict ;
struct ShefferLattStr -> ( ( ) ( ) ShefferStr ) , ( ( ) ( ) LattStr ) ;
aggr ShefferLattStr(# carrier, L_join, L_meet, stroke #) -> ( ( strict ) ( strict ) ShefferLattStr ) ;
end;

definition
attr c1 is strict ;
struct ShefferOrthoLattStr -> ( ( ) ( ) ShefferStr ) , ( ( ) ( ) OrthoLattStr ) ;
aggr ShefferOrthoLattStr(# carrier, L_join, L_meet, Compl, stroke #) -> ( ( strict ) ( strict ) ShefferOrthoLattStr ) ;
end;

definition
func TrivShefferOrthoLattStr -> ( ( ) ( ) ShefferOrthoLattStr ) equals :: SHEFFER1:def 10
 ShefferOrthoLattStr(# 1 : ( ( ) ( ) set ) ,op2 : ( ( V6() V18(K20(1 : ( ( ) ( ) set ) ,1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,1 : ( ( ) ( ) set ) ) ) ( V6() V18(K20(1 : ( ( ) ( ) set ) ,1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,1 : ( ( ) ( ) set ) ) ) M2(K19(K20(K20(1 : ( ( ) ( ) set ) ,1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ,op2 : ( ( V6() V18(K20(1 : ( ( ) ( ) set ) ,1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,1 : ( ( ) ( ) set ) ) ) ( V6() V18(K20(1 : ( ( ) ( ) set ) ,1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,1 : ( ( ) ( ) set ) ) ) M2(K19(K20(K20(1 : ( ( ) ( ) set ) ,1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ,op1 : ( ( V6() V18(1 : ( ( ) ( ) set ) ,1 : ( ( ) ( ) set ) ) ) ( V6() V18(1 : ( ( ) ( ) set ) ,1 : ( ( ) ( ) set ) ) ) M2(K19(K20(1 : ( ( ) ( ) set ) ,1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ,op2 : ( ( V6() V18(K20(1 : ( ( ) ( ) set ) ,1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,1 : ( ( ) ( ) set ) ) ) ( V6() V18(K20(1 : ( ( ) ( ) set ) ,1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,1 : ( ( ) ( ) set ) ) ) M2(K19(K20(K20(1 : ( ( ) ( ) set ) ,1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) #) : ( ( strict ) ( strict ) ShefferOrthoLattStr ) ;
end;

registration
cluster 1 : ( ( ) ( ) set ) -element for ( ( ) ( ) ShefferStr ) ;
cluster 1 : ( ( ) ( ) set ) -element for ( ( ) ( ) ShefferLattStr ) ;
cluster 1 : ( ( ) ( ) set ) -element for ( ( ) ( ) ShefferOrthoLattStr ) ;
end;

definition
let L be ( ( non empty ) ( non empty ) ShefferStr ) ;
let x, y be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
func x | y -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) equals :: SHEFFER1:def 11
 the stroke of L : ( ( cardinal ) ( V26() cardinal ) set ) : ( ( V6() V18(K20( the carrier of L : ( ( cardinal ) ( V26() cardinal ) set ) : ( ( ) ( ) set ) , the carrier of L : ( ( cardinal ) ( V26() cardinal ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) , the carrier of L : ( ( cardinal ) ( V26() cardinal ) set ) : ( ( ) ( ) set ) ) ) ( V6() V18(K20( the carrier of L : ( ( cardinal ) ( V26() cardinal ) set ) : ( ( ) ( ) set ) , the carrier of L : ( ( cardinal ) ( V26() cardinal ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) , the carrier of L : ( ( cardinal ) ( V26() cardinal ) set ) : ( ( ) ( ) set ) ) ) BinOp of the carrier of L : ( ( cardinal ) ( V26() cardinal ) set ) : ( ( ) ( ) set ) ) . (x : ( ( V6() V18(K20(L : ( ( cardinal ) ( V26() cardinal ) set ) ,L : ( ( cardinal ) ( V26() cardinal ) set ) ) : ( ( ) ( ) set ) ,L : ( ( cardinal ) ( V26() cardinal ) set ) ) ) ( V6() V18(K20(L : ( ( cardinal ) ( V26() cardinal ) set ) ,L : ( ( cardinal ) ( V26() cardinal ) set ) ) : ( ( ) ( ) set ) ,L : ( ( cardinal ) ( V26() cardinal ) set ) ) ) M2(K19(K20(K20(L : ( ( cardinal ) ( V26() cardinal ) set ) ,L : ( ( cardinal ) ( V26() cardinal ) set ) ) : ( ( ) ( ) set ) ,L : ( ( cardinal ) ( V26() cardinal ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ,y : ( ( V6() V18(K20(L : ( ( cardinal ) ( V26() cardinal ) set ) ,L : ( ( cardinal ) ( V26() cardinal ) set ) ) : ( ( ) ( ) set ) ,L : ( ( cardinal ) ( V26() cardinal ) set ) ) ) ( V6() V18(K20(L : ( ( cardinal ) ( V26() cardinal ) set ) ,L : ( ( cardinal ) ( V26() cardinal ) set ) ) : ( ( ) ( ) set ) ,L : ( ( cardinal ) ( V26() cardinal ) set ) ) ) M2(K19(K20(K20(L : ( ( cardinal ) ( V26() cardinal ) set ) ,L : ( ( cardinal ) ( V26() cardinal ) set ) ) : ( ( ) ( ) set ) ,L : ( ( cardinal ) ( V26() cardinal ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) ) : ( ( ) ( ) M2( the carrier of L : ( ( cardinal ) ( V26() cardinal ) set ) : ( ( ) ( ) set ) )) ;
end;

definition
let L be ( ( non empty ) ( non empty ) ShefferOrthoLattStr ) ;
attr L is properly_defined means :: SHEFFER1:def 12
( ( for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) | x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ` : ( ( ) ( ) M2( the carrier of L : ( ( cardinal ) ( V26() cardinal ) set ) : ( ( ) ( ) set ) )) ) & ( for x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M2( the carrier of L : ( ( cardinal ) ( V26() cardinal ) set ) : ( ( ) ( ) set ) )) = (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) | x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) | (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) | y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( for x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) M2( the carrier of L : ( ( cardinal ) ( V26() cardinal ) set ) : ( ( ) ( ) set ) )) = (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) | y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) | (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) | y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) & ( for x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) | y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) M2( the carrier of L : ( ( cardinal ) ( V26() cardinal ) set ) : ( ( ) ( ) set ) )) + (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) M2( the carrier of L : ( ( cardinal ) ( V26() cardinal ) set ) : ( ( ) ( ) set ) )) : ( ( ) ( ) M2( the carrier of L : ( ( cardinal ) ( V26() cardinal ) set ) : ( ( ) ( ) set ) )) ) );
end;

definition
let L be ( ( non empty ) ( non empty ) ShefferStr ) ;
attr L is satisfying_Sheffer_1 means :: SHEFFER1:def 13
 for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) | x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) | (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) | x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
attr L is satisfying_Sheffer_2 means :: SHEFFER1:def 14
 for x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) | (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) | (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) | y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) | x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
attr L is satisfying_Sheffer_3 means :: SHEFFER1:def 15
 for x, y, z being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) | (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) | z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) | (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) | (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) | z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = ((y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) | y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) | x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) | ((z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) | z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) | x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
end;

registration
cluster 1 : ( ( ) ( ) set ) -element -> 1 : ( ( ) ( ) set ) -element satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 for ( ( ) ( ) ShefferStr ) ;
end;

registration
cluster 1 : ( ( ) ( ) set ) -element -> 1 : ( ( ) ( ) set ) -element join-commutative join-associative for ( ( ) ( ) \/-SemiLattStr ) ;
cluster 1 : ( ( ) ( ) set ) -element -> 1 : ( ( ) ( ) set ) -element meet-commutative meet-associative for ( ( ) ( ) /\-SemiLattStr ) ;
end;

registration
cluster 1 : ( ( ) ( ) set ) -element -> 1 : ( ( ) ( ) set ) -element meet-absorbing join-absorbing Boolean for ( ( ) ( ) LattStr ) ;
end;

registration
cluster TrivShefferOrthoLattStr : ( ( ) ( ) ShefferOrthoLattStr ) -> 1 : ( ( ) ( ) set ) -element ;
cluster TrivShefferOrthoLattStr : ( ( ) ( ) ShefferOrthoLattStr ) -> ;
end;

registration
cluster non empty Lattice-like Boolean well-complemented properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 for ( ( ) ( ) ShefferOrthoLattStr ) ;
end;

theorem :: SHEFFER1:26
for L being ( ( non empty Lattice-like Boolean well-complemented properly_defined ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V68() complemented Boolean Robbins Huntington join-idempotent well-complemented upper-bounded' lower-bounded' distributive' complemented' properly_defined ) ShefferOrthoLattStr ) holds L : ( ( non empty Lattice-like Boolean well-complemented properly_defined ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V68() complemented Boolean Robbins Huntington join-idempotent well-complemented upper-bounded' lower-bounded' distributive' complemented' properly_defined ) ShefferOrthoLattStr ) is satisfying_Sheffer_1 ;

theorem :: SHEFFER1:27
for L being ( ( non empty Lattice-like Boolean well-complemented properly_defined ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V68() complemented Boolean Robbins Huntington join-idempotent well-complemented upper-bounded' lower-bounded' distributive' complemented' properly_defined ) ShefferOrthoLattStr ) holds L : ( ( non empty Lattice-like Boolean well-complemented properly_defined ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V68() complemented Boolean Robbins Huntington join-idempotent well-complemented upper-bounded' lower-bounded' distributive' complemented' properly_defined ) ShefferOrthoLattStr ) is satisfying_Sheffer_2 ;

theorem :: SHEFFER1:28
for L being ( ( non empty Lattice-like Boolean well-complemented properly_defined ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V68() complemented Boolean Robbins Huntington join-idempotent well-complemented upper-bounded' lower-bounded' distributive' complemented' properly_defined ) ShefferOrthoLattStr ) holds L : ( ( non empty Lattice-like Boolean well-complemented properly_defined ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V68() complemented Boolean Robbins Huntington join-idempotent well-complemented upper-bounded' lower-bounded' distributive' complemented' properly_defined ) ShefferOrthoLattStr ) is satisfying_Sheffer_3 ;

definition
let L be ( ( non empty ) ( non empty ) ShefferStr ) ;
let a be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
func a " -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) equals :: SHEFFER1:def 16
a : ( ( V6() V18(K20(L : ( ( cardinal ) ( V26() cardinal ) set ) ,L : ( ( cardinal ) ( V26() cardinal ) set ) ) : ( ( ) ( ) set ) ,L : ( ( cardinal ) ( V26() cardinal ) set ) ) ) ( V6() V18(K20(L : ( ( cardinal ) ( V26() cardinal ) set ) ,L : ( ( cardinal ) ( V26() cardinal ) set ) ) : ( ( ) ( ) set ) ,L : ( ( cardinal ) ( V26() cardinal ) set ) ) ) M2(K19(K20(K20(L : ( ( cardinal ) ( V26() cardinal ) set ) ,L : ( ( cardinal ) ( V26() cardinal ) set ) ) : ( ( ) ( ) set ) ,L : ( ( cardinal ) ( V26() cardinal ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) | a : ( ( V6() V18(K20(L : ( ( cardinal ) ( V26() cardinal ) set ) ,L : ( ( cardinal ) ( V26() cardinal ) set ) ) : ( ( ) ( ) set ) ,L : ( ( cardinal ) ( V26() cardinal ) set ) ) ) ( V6() V18(K20(L : ( ( cardinal ) ( V26() cardinal ) set ) ,L : ( ( cardinal ) ( V26() cardinal ) set ) ) : ( ( ) ( ) set ) ,L : ( ( cardinal ) ( V26() cardinal ) set ) ) ) M2(K19(K20(K20(L : ( ( cardinal ) ( V26() cardinal ) set ) ,L : ( ( cardinal ) ( V26() cardinal ) set ) ) : ( ( ) ( ) set ) ,L : ( ( cardinal ) ( V26() cardinal ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
end;

theorem :: SHEFFER1:29
for L being ( ( non empty satisfying_Sheffer_3 ) ( non empty satisfying_Sheffer_3 ) ShefferOrthoLattStr )
for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) | (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) | z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) " : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = ((y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ") : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) | x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) | ((z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ") : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) | x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: SHEFFER1:30
for L being ( ( non empty satisfying_Sheffer_1 ) ( non empty satisfying_Sheffer_1 ) ShefferOrthoLattStr )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ") : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) " : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: SHEFFER1:31
for L being ( ( non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ) ( non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ) ShefferOrthoLattStr )
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) | y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) | x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: SHEFFER1:32
for L being ( ( non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ) ( non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ) ShefferOrthoLattStr )
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) | (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) | x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) | (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) | y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: SHEFFER1:33
for L being ( ( non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ) ( non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ) ShefferOrthoLattStr ) holds L : ( ( non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ) ( non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ) ShefferOrthoLattStr ) is join-commutative ;

theorem :: SHEFFER1:34
for L being ( ( non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ) ( non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ) ShefferOrthoLattStr ) holds L : ( ( non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ) ( non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ) ShefferOrthoLattStr ) is meet-commutative ;

theorem :: SHEFFER1:35
for L being ( ( non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ) ( non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ) ShefferOrthoLattStr ) holds L : ( ( non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ) ( non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ) ShefferOrthoLattStr ) is distributive ;

theorem :: SHEFFER1:36
for L being ( ( non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ) ( non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ) ShefferOrthoLattStr ) holds L : ( ( non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ) ( non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ) ShefferOrthoLattStr ) is distributive' ;

theorem :: SHEFFER1:37
for L being ( ( non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ) ( non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ) ShefferOrthoLattStr ) holds L : ( ( non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ) ( non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ) ShefferOrthoLattStr ) is ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V68() complemented Boolean upper-bounded' lower-bounded' distributive' complemented' ) Lattice) ;