:: SHEFFER1 semantic presentation begin theorem Th1: :: SHEFFER1:1 for L being non empty join-commutative join-associative Huntington ComplLLattStr for a, b being Element of L holds (a + b) ` = (a `) *' (b `) proof let L be non empty join-commutative join-associative Huntington ComplLLattStr ; ::_thesis: for a, b being Element of L holds (a + b) ` = (a `) *' (b `) let a, b be Element of L; ::_thesis: (a + b) ` = (a `) *' (b `) a + b = ((a `) *' (b `)) ` by ROBBINS1:17; hence (a + b) ` = (a `) *' (b `) by ROBBINS1:3; ::_thesis: verum end; begin definition let IT be non empty LattStr ; attrIT is upper-bounded' means :Def1: :: SHEFFER1:def 1 ex c being Element of IT st for a being Element of IT holds ( c "/\" a = a & a "/\" c = a ); end; :: deftheorem Def1 defines upper-bounded' SHEFFER1:def_1_:_ for IT being non empty LattStr holds ( IT is upper-bounded' iff ex c being Element of IT st for a being Element of IT holds ( c "/\" a = a & a "/\" c = a ) ); definition let L be non empty LattStr ; assume A1: L is upper-bounded' ; func Top' L -> Element of L means :Def2: :: SHEFFER1:def 2 for a being Element of L holds ( it "/\" a = a & a "/\" it = a ); existence ex b1 being Element of L st for a being Element of L holds ( b1 "/\" a = a & a "/\" b1 = a ) by A1, Def1; uniqueness for b1, b2 being Element of L st ( for a being Element of L holds ( b1 "/\" a = a & a "/\" b1 = a ) ) & ( for a being Element of L holds ( b2 "/\" a = a & a "/\" b2 = a ) ) holds b1 = b2 proof let c1, c2 be Element of L; ::_thesis: ( ( for a being Element of L holds ( c1 "/\" a = a & a "/\" c1 = a ) ) & ( for a being Element of L holds ( c2 "/\" a = a & a "/\" c2 = a ) ) implies c1 = c2 ) assume that A2: for a being Element of L holds ( c1 "/\" a = a & a "/\" c1 = a ) and A3: for a being Element of L holds ( c2 "/\" a = a & a "/\" c2 = a ) ; ::_thesis: c1 = c2 thus c1 = c2 "/\" c1 by A3 .= c2 by A2 ; ::_thesis: verum end; end; :: deftheorem Def2 defines Top' SHEFFER1:def_2_:_ for L being non empty LattStr st L is upper-bounded' holds for b2 being Element of L holds ( b2 = Top' L iff for a being Element of L holds ( b2 "/\" a = a & a "/\" b2 = a ) ); definition let IT be non empty LattStr ; attrIT is lower-bounded' means :Def3: :: SHEFFER1:def 3 ex c being Element of IT st for a being Element of IT holds ( c "\/" a = a & a "\/" c = a ); end; :: deftheorem Def3 defines lower-bounded' SHEFFER1:def_3_:_ for IT being non empty LattStr holds ( IT is lower-bounded' iff ex c being Element of IT st for a being Element of IT holds ( c "\/" a = a & a "\/" c = a ) ); definition let L be non empty LattStr ; assume A1: L is lower-bounded' ; func Bot' L -> Element of L means :Def4: :: SHEFFER1:def 4 for a being Element of L holds ( it "\/" a = a & a "\/" it = a ); existence ex b1 being Element of L st for a being Element of L holds ( b1 "\/" a = a & a "\/" b1 = a ) by A1, Def3; uniqueness for b1, b2 being Element of L st ( for a being Element of L holds ( b1 "\/" a = a & a "\/" b1 = a ) ) & ( for a being Element of L holds ( b2 "\/" a = a & a "\/" b2 = a ) ) holds b1 = b2 proof let c1, c2 be Element of L; ::_thesis: ( ( for a being Element of L holds ( c1 "\/" a = a & a "\/" c1 = a ) ) & ( for a being Element of L holds ( c2 "\/" a = a & a "\/" c2 = a ) ) implies c1 = c2 ) assume that A2: for a being Element of L holds ( c1 "\/" a = a & a "\/" c1 = a ) and A3: for a being Element of L holds ( c2 "\/" a = a & a "\/" c2 = a ) ; ::_thesis: c1 = c2 thus c1 = c2 "\/" c1 by A3 .= c2 by A2 ; ::_thesis: verum end; end; :: deftheorem Def4 defines Bot' SHEFFER1:def_4_:_ for L being non empty LattStr st L is lower-bounded' holds for b2 being Element of L holds ( b2 = Bot' L iff for a being Element of L holds ( b2 "\/" a = a & a "\/" b2 = a ) ); definition let IT be non empty LattStr ; attrIT is distributive' means :Def5: :: SHEFFER1:def 5 for a, b, c being Element of IT holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c); end; :: deftheorem Def5 defines distributive' SHEFFER1:def_5_:_ for IT being non empty LattStr holds ( IT is distributive' iff for a, b, c being Element of IT holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) ); definition let L be non empty LattStr ; let a, b be Element of L; preda is_a_complement'_of b means :Def6: :: SHEFFER1:def 6 ( b "\/" a = Top' L & a "\/" b = Top' L & b "/\" a = Bot' L & a "/\" b = Bot' L ); end; :: deftheorem Def6 defines is_a_complement'_of SHEFFER1:def_6_:_ for L being non empty LattStr for a, b being Element of L holds ( a is_a_complement'_of b iff ( b "\/" a = Top' L & a "\/" b = Top' L & b "/\" a = Bot' L & a "/\" b = Bot' L ) ); definition let IT be non empty LattStr ; attrIT is complemented' means :Def7: :: SHEFFER1:def 7 for b being Element of IT ex a being Element of IT st a is_a_complement'_of b; end; :: deftheorem Def7 defines complemented' SHEFFER1:def_7_:_ for IT being non empty LattStr holds ( IT is complemented' iff for b being Element of IT ex a being Element of IT st a is_a_complement'_of b ); definition let L be non empty LattStr ; let x be Element of L; assume A1: ( L is complemented' & L is distributive & L is upper-bounded' & L is meet-commutative ) ; funcx `# -> Element of L means :Def8: :: SHEFFER1:def 8 it is_a_complement'_of x; existence ex b1 being Element of L st b1 is_a_complement'_of x by A1, Def7; uniqueness for b1, b2 being Element of L st b1 is_a_complement'_of x & b2 is_a_complement'_of x holds b1 = b2 proof let a, b be Element of L; ::_thesis: ( a is_a_complement'_of x & b is_a_complement'_of x implies a = b ) assume that A2: a is_a_complement'_of x and A3: b is_a_complement'_of x ; ::_thesis: a = b b = b "/\" (Top' L) by A1, Def2 .= b "/\" (x "\/" a) by A2, Def6 .= (b "/\" x) "\/" (b "/\" a) by A1, LATTICES:def_11 .= (x "/\" b) "\/" (b "/\" a) by A1, LATTICES:def_6 .= (x "/\" b) "\/" (a "/\" b) by A1, LATTICES:def_6 .= (Bot' L) "\/" (a "/\" b) by A3, Def6 .= (a "/\" x) "\/" (a "/\" b) by A2, Def6 .= a "/\" (x "\/" b) by A1, LATTICES:def_11 .= a "/\" (Top' L) by A3, Def6 .= a by A1, Def2 ; hence a = b ; ::_thesis: verum end; end; :: deftheorem Def8 defines `# SHEFFER1:def_8_:_ for L being non empty LattStr for x being Element of L st L is complemented' & L is distributive & L is upper-bounded' & L is meet-commutative holds for b3 being Element of L holds ( b3 = x `# iff b3 is_a_complement'_of x ); registration cluster non empty V45() V46() 1 -element Lattice-like Boolean join-idempotent upper-bounded' lower-bounded' distributive' complemented' for LattStr ; existence ex b1 being 1 -element LattStr st ( b1 is Boolean & b1 is join-idempotent & b1 is upper-bounded' & b1 is complemented' & b1 is distributive' & b1 is lower-bounded' & b1 is Lattice-like ) proof set L = the 1 -element Lattice; A1: the 1 -element Lattice is lower-bounded proof set x = the Element of the 1 -element Lattice; for y being Element of the 1 -element Lattice holds ( the Element of the 1 -element Lattice "/\" y = the Element of the 1 -element Lattice & y "/\" the Element of the 1 -element Lattice = the Element of the 1 -element Lattice ) by STRUCT_0:def_10; hence the 1 -element Lattice is lower-bounded by LATTICES:def_13; ::_thesis: verum end; A2: the 1 -element Lattice is upper-bounded proof set x = the Element of the 1 -element Lattice; for y being Element of the 1 -element Lattice holds ( the Element of the 1 -element Lattice "\/" y = the Element of the 1 -element Lattice & y "\/" the Element of the 1 -element Lattice = the Element of the 1 -element Lattice ) by STRUCT_0:def_10; hence the 1 -element Lattice is upper-bounded by LATTICES:def_14; ::_thesis: verum end; for b being Element of the 1 -element Lattice ex a being Element of the 1 -element Lattice st a is_a_complement_of b proof let b be Element of the 1 -element Lattice; ::_thesis: ex a being Element of the 1 -element Lattice st a is_a_complement_of b take a = b; ::_thesis: a is_a_complement_of b ( b "\/" a = Top the 1 -element Lattice & b "/\" a = Bottom the 1 -element Lattice ) by STRUCT_0:def_10; hence a is_a_complement_of b by LATTICES:def_18; ::_thesis: verum end; then A3: the 1 -element Lattice is complemented by LATTICES:def_19; A4: the 1 -element Lattice is join-idempotent proof let x be Element of the 1 -element Lattice; :: according to ROBBINS1:def_7 ::_thesis: x "\/" x = x thus x "\/" x = x ; ::_thesis: verum end; for b being Element of the 1 -element Lattice ex a being Element of the 1 -element Lattice st a is_a_complement'_of b proof let b be Element of the 1 -element Lattice; ::_thesis: ex a being Element of the 1 -element Lattice st a is_a_complement'_of b take a = b; ::_thesis: a is_a_complement'_of b ( b "\/" a = Top' the 1 -element Lattice & b "/\" a = Bot' the 1 -element Lattice ) by STRUCT_0:def_10; hence a is_a_complement'_of b by Def6; ::_thesis: verum end; then A5: the 1 -element Lattice is complemented' by Def7; for a, b, c being Element of the 1 -element Lattice holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) by STRUCT_0:def_10; then A6: the 1 -element Lattice is distributive by LATTICES:def_11; A7: the 1 -element Lattice is lower-bounded' proof set x = the Element of the 1 -element Lattice; for y being Element of the 1 -element Lattice holds ( the Element of the 1 -element Lattice "\/" y = y & y "\/" the Element of the 1 -element Lattice = y ) by STRUCT_0:def_10; hence the 1 -element Lattice is lower-bounded' by Def3; ::_thesis: verum end; A8: the 1 -element Lattice is upper-bounded' proof set x = the Element of the 1 -element Lattice; for y being Element of the 1 -element Lattice holds ( the Element of the 1 -element Lattice "/\" y = y & y "/\" the Element of the 1 -element Lattice = y ) by STRUCT_0:def_10; hence the 1 -element Lattice is upper-bounded' by Def1; ::_thesis: verum end; for a, b, c being Element of the 1 -element Lattice holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) by STRUCT_0:def_10; then the 1 -element Lattice is distributive' by Def5; hence ex b1 being 1 -element LattStr st ( b1 is Boolean & b1 is join-idempotent & b1 is upper-bounded' & b1 is complemented' & b1 is distributive' & b1 is lower-bounded' & b1 is Lattice-like ) by A3, A6, A1, A2, A4, A8, A5, A7; ::_thesis: verum end; end; theorem Th2: :: SHEFFER1:2 for L being non empty join-commutative meet-commutative distributive upper-bounded' distributive' complemented' LattStr for x being Element of L holds x "\/" (x `#) = Top' L proof let L be non empty join-commutative meet-commutative distributive upper-bounded' distributive' complemented' LattStr ; ::_thesis: for x being Element of L holds x "\/" (x `#) = Top' L let x be Element of L; ::_thesis: x "\/" (x `#) = Top' L x `# is_a_complement'_of x by Def8; hence x "\/" (x `#) = Top' L by Def6; ::_thesis: verum end; theorem Th3: :: SHEFFER1:3 for L being non empty join-commutative meet-commutative distributive upper-bounded' distributive' complemented' LattStr for x being Element of L holds x "/\" (x `#) = Bot' L proof let L be non empty join-commutative meet-commutative distributive upper-bounded' distributive' complemented' LattStr ; ::_thesis: for x being Element of L holds x "/\" (x `#) = Bot' L let x be Element of L; ::_thesis: x "/\" (x `#) = Bot' L x `# is_a_complement'_of x by Def8; hence x "/\" (x `#) = Bot' L by Def6; ::_thesis: verum end; theorem Th4: :: SHEFFER1:4 for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' distributive' complemented' LattStr for x being Element of L holds x "\/" (Top' L) = Top' L proof let L be non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' distributive' complemented' LattStr ; ::_thesis: for x being Element of L holds x "\/" (Top' L) = Top' L let x be Element of L; ::_thesis: x "\/" (Top' L) = Top' L x "\/" (Top' L) = (x "\/" (Top' L)) "/\" (Top' L) by Def2 .= (x "\/" (Top' L)) "/\" (x "\/" (x `#)) by Th2 .= x "\/" ((Top' L) "/\" (x `#)) by Def5 .= x "\/" (x `#) by Def2 .= Top' L by Th2 ; hence x "\/" (Top' L) = Top' L ; ::_thesis: verum end; theorem Th5: :: SHEFFER1:5 for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr for x being Element of L holds x "/\" (Bot' L) = Bot' L proof let L be non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr ; ::_thesis: for x being Element of L holds x "/\" (Bot' L) = Bot' L let x be Element of L; ::_thesis: x "/\" (Bot' L) = Bot' L x "/\" (Bot' L) = (x "/\" (Bot' L)) "\/" (Bot' L) by Def4 .= (x "/\" (Bot' L)) "\/" (x "/\" (x `#)) by Th3 .= x "/\" ((Bot' L) "\/" (x `#)) by LATTICES:def_11 .= x "/\" (x `#) by Def4 .= Bot' L by Th3 ; hence x "/\" (Bot' L) = Bot' L ; ::_thesis: verum end; theorem Th6: :: SHEFFER1:6 for L being non empty join-commutative meet-commutative meet-absorbing join-absorbing distributive join-idempotent LattStr for x, y, z being Element of L holds ((x "\/" y) "\/" z) "/\" x = x proof let L be non empty join-commutative meet-commutative meet-absorbing join-absorbing distributive join-idempotent LattStr ; ::_thesis: for x, y, z being Element of L holds ((x "\/" y) "\/" z) "/\" x = x let x, y, z be Element of L; ::_thesis: ((x "\/" y) "\/" z) "/\" x = x ((x "\/" y) "\/" z) "/\" x = (x "/\" (x "\/" y)) "\/" (x "/\" z) by LATTICES:def_11 .= ((x "/\" x) "\/" (x "/\" y)) "\/" (x "/\" z) by LATTICES:def_11 .= (x "\/" (x "/\" y)) "\/" (x "/\" z) .= x "\/" (x "/\" z) by LATTICES:def_8 .= x by LATTICES:def_8 ; hence ((x "\/" y) "\/" z) "/\" x = x ; ::_thesis: verum end; theorem Th7: :: SHEFFER1:7 for L being non empty join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent distributive' LattStr for x, y, z being Element of L holds ((x "/\" y) "/\" z) "\/" x = x proof let L be non empty join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent distributive' LattStr ; ::_thesis: for x, y, z being Element of L holds ((x "/\" y) "/\" z) "\/" x = x let x, y, z be Element of L; ::_thesis: ((x "/\" y) "/\" z) "\/" x = x ((x "/\" y) "/\" z) "\/" x = (x "\/" (x "/\" y)) "/\" (x "\/" z) by Def5 .= ((x "\/" x) "/\" (x "\/" y)) "/\" (x "\/" z) by Def5 .= (x "/\" (x "\/" y)) "/\" (x "\/" z) .= x "/\" (x "\/" z) by LATTICES:def_9 .= x by LATTICES:def_9 ; hence ((x "/\" y) "/\" z) "\/" x = x ; ::_thesis: verum end; definition let G be non empty /\-SemiLattStr ; attrG is meet-idempotent means :Def9: :: SHEFFER1:def 9 for x being Element of G holds x "/\" x = x; end; :: deftheorem Def9 defines meet-idempotent SHEFFER1:def_9_:_ for G being non empty /\-SemiLattStr holds ( G is meet-idempotent iff for x being Element of G holds x "/\" x = x ); theorem Th8: :: SHEFFER1:8 for L being non empty join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' complemented' LattStr holds L is meet-idempotent proof let L be non empty join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' complemented' LattStr ; ::_thesis: L is meet-idempotent now__::_thesis:_for_x_being_Element_of_L_holds_x_"/\"_x_=_x let x be Element of L; ::_thesis: x "/\" x = x thus x "/\" x = (x "/\" x) "\/" (Bot' L) by Def4 .= (x "/\" x) "\/" (x "/\" (x `#)) by Th3 .= x "/\" (x "\/" (x `#)) by LATTICES:def_11 .= x "/\" (Top' L) by Th2 .= x by Def2 ; ::_thesis: verum end; hence L is meet-idempotent by Def9; ::_thesis: verum end; theorem Th9: :: SHEFFER1:9 for L being non empty join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' complemented' LattStr holds L is join-idempotent proof let L be non empty join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' complemented' LattStr ; ::_thesis: L is join-idempotent let x be Element of L; :: according to ROBBINS1:def_7 ::_thesis: x "\/" x = x thus x "\/" x = (x "\/" x) "/\" (Top' L) by Def2 .= (x "\/" x) "/\" (x "\/" (x `#)) by Th2 .= x "\/" (x "/\" (x `#)) by Def5 .= x "\/" (Bot' L) by Th3 .= x by Def4 ; ::_thesis: verum end; theorem Th10: :: SHEFFER1:10 for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' distributive' complemented' LattStr holds L is meet-absorbing proof let L be non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' distributive' complemented' LattStr ; ::_thesis: L is meet-absorbing let y, x be Element of L; :: according to LATTICES:def_8 ::_thesis: (y "/\" x) "\/" x = x x "\/" (x "/\" y) = ((Top' L) "/\" x) "\/" (x "/\" y) by Def2 .= x "/\" ((Top' L) "\/" y) by LATTICES:def_11 .= x "/\" (Top' L) by Th4 .= x by Def2 ; hence (y "/\" x) "\/" x = x ; ::_thesis: verum end; theorem Th11: :: SHEFFER1:11 for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr holds L is join-absorbing proof let L be non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr ; ::_thesis: L is join-absorbing let x, y be Element of L; :: according to LATTICES:def_9 ::_thesis: x "/\" (x "\/" y) = x A1: L is meet-idempotent by Th8; A2: L is meet-absorbing by Th10; x "/\" (x "\/" y) = (x "/\" x) "\/" (x "/\" y) by LATTICES:def_11 .= x "\/" (x "/\" y) by A1, Def9 .= x by A2, LATTICES:def_8 ; hence x "/\" (x "\/" y) = x ; ::_thesis: verum end; theorem Th12: :: SHEFFER1:12 for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr holds L is upper-bounded proof let L be non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr ; ::_thesis: L is upper-bounded ex c being Element of L st for a being Element of L holds ( c "\/" a = c & a "\/" c = c ) proof take Top' L ; ::_thesis: for a being Element of L holds ( (Top' L) "\/" a = Top' L & a "\/" (Top' L) = Top' L ) let a be Element of L; ::_thesis: ( (Top' L) "\/" a = Top' L & a "\/" (Top' L) = Top' L ) thus ( (Top' L) "\/" a = Top' L & a "\/" (Top' L) = Top' L ) by Th4; ::_thesis: verum end; hence L is upper-bounded by LATTICES:def_14; ::_thesis: verum end; theorem Th13: :: SHEFFER1:13 for L being non empty Lattice-like Boolean LattStr holds L is upper-bounded' proof let L be non empty Lattice-like Boolean LattStr ; ::_thesis: L is upper-bounded' ex c being Element of L st for a being Element of L holds ( c "/\" a = a & a "/\" c = a ) proof take c = Top L; ::_thesis: for a being Element of L holds ( c "/\" a = a & a "/\" c = a ) let a be Element of L; ::_thesis: ( c "/\" a = a & a "/\" c = a ) a [= c by LATTICES:19; hence ( c "/\" a = a & a "/\" c = a ) by LATTICES:4; ::_thesis: verum end; hence L is upper-bounded' by Def1; ::_thesis: verum end; theorem Th14: :: SHEFFER1:14 for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr holds L is lower-bounded proof let L be non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr ; ::_thesis: L is lower-bounded ex c being Element of L st for a being Element of L holds ( c "/\" a = c & a "/\" c = c ) proof take Bot' L ; ::_thesis: for a being Element of L holds ( (Bot' L) "/\" a = Bot' L & a "/\" (Bot' L) = Bot' L ) let a be Element of L; ::_thesis: ( (Bot' L) "/\" a = Bot' L & a "/\" (Bot' L) = Bot' L ) thus ( (Bot' L) "/\" a = Bot' L & a "/\" (Bot' L) = Bot' L ) by Th5; ::_thesis: verum end; hence L is lower-bounded by LATTICES:def_13; ::_thesis: verum end; theorem Th15: :: SHEFFER1:15 for L being non empty Lattice-like Boolean LattStr holds L is lower-bounded' proof let L be non empty Lattice-like Boolean LattStr ; ::_thesis: L is lower-bounded' ex c being Element of L st for a being Element of L holds ( c "\/" a = a & a "\/" c = a ) proof take c = Bottom L; ::_thesis: for a being Element of L holds ( c "\/" a = a & a "\/" c = a ) let a be Element of L; ::_thesis: ( c "\/" a = a & a "\/" c = a ) c [= a by LATTICES:16; hence ( c "\/" a = a & a "\/" c = a ) by LATTICES:def_3; ::_thesis: verum end; hence L is lower-bounded' by Def3; ::_thesis: verum end; theorem Th16: :: SHEFFER1:16 for L being non empty join-commutative meet-commutative meet-absorbing join-absorbing distributive join-idempotent LattStr holds L is join-associative proof let L be non empty join-commutative meet-commutative meet-absorbing join-absorbing distributive join-idempotent LattStr ; ::_thesis: L is join-associative let x, y, z be Element of L; :: according to LATTICES:def_5 ::_thesis: x "\/" (y "\/" z) = (x "\/" y) "\/" z A1: ((y "\/" z) "\/" x) "/\" y = (y "/\" (y "\/" z)) "\/" (y "/\" x) by LATTICES:def_11 .= ((y "/\" y) "\/" (y "/\" z)) "\/" (y "/\" x) by LATTICES:def_11 .= (y "\/" (y "/\" z)) "\/" (y "/\" x) .= y "\/" (y "/\" x) by LATTICES:def_8 .= y by LATTICES:def_8 ; A2: ((x "\/" y) "\/" z) "/\" x = x by Th6; x "\/" (y "\/" z) = (x "\/" y) "\/" z proof set A = ((x "\/" y) "\/" z) "/\" (x "\/" (y "\/" z)); A3: ((x "\/" y) "\/" z) "/\" (x "\/" (y "\/" z)) = ((x "\/" y) "/\" (x "\/" (y "\/" z))) "\/" (z "/\" (x "\/" (y "\/" z))) by LATTICES:def_11 .= ((x "\/" y) "/\" (x "\/" (y "\/" z))) "\/" z by Th6 .= ((x "/\" (x "\/" (y "\/" z))) "\/" (y "/\" (x "\/" (y "\/" z)))) "\/" z by LATTICES:def_11 .= (x "\/" y) "\/" z by A1, LATTICES:def_9 ; ((x "\/" y) "\/" z) "/\" (x "\/" (y "\/" z)) = (((x "\/" y) "\/" z) "/\" x) "\/" (((x "\/" y) "\/" z) "/\" (y "\/" z)) by LATTICES:def_11 .= x "\/" ((((x "\/" y) "\/" z) "/\" y) "\/" (((x "\/" y) "\/" z) "/\" z)) by A2, LATTICES:def_11 .= x "\/" (y "\/" (((x "\/" y) "\/" z) "/\" z)) by Th6 .= x "\/" (y "\/" (((x "\/" y) "/\" z) "\/" (z "/\" z))) by LATTICES:def_11 .= x "\/" (y "\/" (((x "\/" y) "/\" z) "\/" z)) .= x "\/" (y "\/" z) by LATTICES:def_8 ; hence x "\/" (y "\/" z) = (x "\/" y) "\/" z by A3; ::_thesis: verum end; hence x "\/" (y "\/" z) = (x "\/" y) "\/" z ; ::_thesis: verum end; theorem Th17: :: SHEFFER1:17 for L being non empty join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent distributive' LattStr holds L is meet-associative proof let L be non empty join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent distributive' LattStr ; ::_thesis: L is meet-associative let x, y, z be Element of L; :: according to LATTICES:def_7 ::_thesis: x "/\" (y "/\" z) = (x "/\" y) "/\" z A1: ((x "/\" y) "/\" z) "\/" x = x by Th7; A2: ((y "/\" z) "/\" x) "\/" y = (y "\/" (y "/\" z)) "/\" (y "\/" x) by Def5 .= ((y "\/" y) "/\" (y "\/" z)) "/\" (y "\/" x) by Def5 .= (y "/\" (y "\/" z)) "/\" (y "\/" x) .= y "/\" (y "\/" x) by LATTICES:def_9 .= y by LATTICES:def_9 ; x "/\" (y "/\" z) = (x "/\" y) "/\" z proof set A = ((x "/\" y) "/\" z) "\/" (x "/\" (y "/\" z)); A3: ((x "/\" y) "/\" z) "\/" (x "/\" (y "/\" z)) = ((x "/\" y) "\/" (x "/\" (y "/\" z))) "/\" (z "\/" (x "/\" (y "/\" z))) by Def5 .= ((x "/\" y) "\/" (x "/\" (y "/\" z))) "/\" z by Th7 .= ((x "\/" (x "/\" (y "/\" z))) "/\" (y "\/" (x "/\" (y "/\" z)))) "/\" z by Def5 .= (x "/\" y) "/\" z by A2, LATTICES:def_8 ; ((x "/\" y) "/\" z) "\/" (x "/\" (y "/\" z)) = (((x "/\" y) "/\" z) "\/" x) "/\" (((x "/\" y) "/\" z) "\/" (y "/\" z)) by Def5 .= x "/\" ((((x "/\" y) "/\" z) "\/" y) "/\" (((x "/\" y) "/\" z) "\/" z)) by A1, Def5 .= x "/\" (y "/\" (((x "/\" y) "/\" z) "\/" z)) by Th7 .= x "/\" (y "/\" (((x "/\" y) "\/" z) "/\" (z "\/" z))) by Def5 .= x "/\" (y "/\" (((x "/\" y) "\/" z) "/\" z)) .= x "/\" (y "/\" z) by LATTICES:def_9 ; hence x "/\" (y "/\" z) = (x "/\" y) "/\" z by A3; ::_thesis: verum end; hence x "/\" (y "/\" z) = (x "/\" y) "/\" z ; ::_thesis: verum end; theorem Th18: :: SHEFFER1:18 for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr holds Top L = Top' L proof let L be non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr ; ::_thesis: Top L = Top' L set Y = Top' L; ( L is upper-bounded & ( for a being Element of L holds ( (Top' L) "\/" a = Top' L & a "\/" (Top' L) = Top' L ) ) ) by Th4, Th12; hence Top L = Top' L by LATTICES:def_17; ::_thesis: verum end; theorem Th19: :: SHEFFER1:19 for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr holds Bottom L = Bot' L proof let L be non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr ; ::_thesis: Bottom L = Bot' L set Y = Bot' L; ( L is lower-bounded & ( for a being Element of L holds ( (Bot' L) "/\" a = Bot' L & a "/\" (Bot' L) = Bot' L ) ) ) by Th5, Th14; hence Bottom L = Bot' L by LATTICES:def_16; ::_thesis: verum end; theorem Th20: :: SHEFFER1:20 for L being non empty Lattice-like Boolean distributive' LattStr holds Top L = Top' L proof let L be non empty Lattice-like Boolean distributive' LattStr ; ::_thesis: Top L = Top' L set Y = Top L; ( L is upper-bounded' & ( for a being Element of L holds ( (Top L) "/\" a = a & a "/\" (Top L) = a ) ) ) by Th13; hence Top L = Top' L by Def2; ::_thesis: verum end; theorem Th21: :: SHEFFER1:21 for L being non empty Lattice-like distributive lower-bounded upper-bounded complemented Boolean distributive' LattStr holds Bottom L = Bot' L proof let L be non empty Lattice-like distributive lower-bounded upper-bounded complemented Boolean distributive' LattStr ; ::_thesis: Bottom L = Bot' L set Y = Bottom L; ( L is lower-bounded' & ( for a being Element of L holds ( (Bottom L) "\/" a = a & a "\/" (Bottom L) = a ) ) ) by Th15; hence Bottom L = Bot' L by Def4; ::_thesis: verum end; theorem :: SHEFFER1:22 for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr for x, y being Element of L holds ( x is_a_complement'_of y iff x is_a_complement_of y ) proof let L be non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr ; ::_thesis: for x, y being Element of L holds ( x is_a_complement'_of y iff x is_a_complement_of y ) let x, y be Element of L; ::_thesis: ( x is_a_complement'_of y iff x is_a_complement_of y ) hereby ::_thesis: ( x is_a_complement_of y implies x is_a_complement'_of y ) assume A1: x is_a_complement'_of y ; ::_thesis: x is_a_complement_of y then x "/\" y = Bot' L by Def6; then A2: x "/\" y = Bottom L by Th19; x "\/" y = Top' L by A1, Def6; then x "\/" y = Top L by Th18; hence x is_a_complement_of y by A2, LATTICES:def_18; ::_thesis: verum end; assume A3: x is_a_complement_of y ; ::_thesis: x is_a_complement'_of y then x "/\" y = Bottom L by LATTICES:def_18; then A4: x "/\" y = Bot' L by Th19; x "\/" y = Top L by A3, LATTICES:def_18; then x "\/" y = Top' L by Th18; hence x is_a_complement'_of y by A4, Def6; ::_thesis: verum end; theorem Th23: :: SHEFFER1:23 for L being non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr holds L is complemented proof let L be non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr ; ::_thesis: L is complemented for b being Element of L ex a being Element of L st a is_a_complement_of b proof let b be Element of L; ::_thesis: ex a being Element of L st a is_a_complement_of b consider a being Element of L such that A1: a is_a_complement'_of b by Def7; b "/\" a = Bot' L by A1, Def6; then A2: b "/\" a = Bottom L by Th19; b "\/" a = Top' L by A1, Def6; then b "\/" a = Top L by Th18; then a is_a_complement_of b by A2, LATTICES:def_18; hence ex a being Element of L st a is_a_complement_of b ; ::_thesis: verum end; hence L is complemented by LATTICES:def_19; ::_thesis: verum end; theorem Th24: :: SHEFFER1:24 for L being non empty Lattice-like Boolean upper-bounded' lower-bounded' distributive' LattStr holds L is complemented' proof let L be non empty Lattice-like Boolean upper-bounded' lower-bounded' distributive' LattStr ; ::_thesis: L is complemented' for b being Element of L ex a being Element of L st a is_a_complement'_of b proof let b be Element of L; ::_thesis: ex a being Element of L st a is_a_complement'_of b consider a being Element of L such that A1: a is_a_complement_of b by LATTICES:def_19; b "/\" a = Bottom L by A1, LATTICES:def_18; then A2: b "/\" a = Bot' L by Th21; b "\/" a = Top L by A1, LATTICES:def_18; then b "\/" a = Top' L by Th20; then a is_a_complement'_of b by A2, Def6; hence ex a being Element of L st a is_a_complement'_of b ; ::_thesis: verum end; hence L is complemented' by Def7; ::_thesis: verum end; theorem Th25: :: SHEFFER1:25 for L being non empty LattStr holds ( L is Boolean Lattice iff ( L is lower-bounded' & L is upper-bounded' & L is join-commutative & L is meet-commutative & L is distributive & L is distributive' & L is complemented' ) ) proof let L be non empty LattStr ; ::_thesis: ( L is Boolean Lattice iff ( L is lower-bounded' & L is upper-bounded' & L is join-commutative & L is meet-commutative & L is distributive & L is distributive' & L is complemented' ) ) thus ( L is Boolean Lattice implies ( L is lower-bounded' & L is upper-bounded' & L is join-commutative & L is meet-commutative & L is distributive & L is distributive' & L is complemented' ) ) ::_thesis: ( L is lower-bounded' & L is upper-bounded' & L is join-commutative & L is meet-commutative & L is distributive & L is distributive' & L is complemented' implies L is Boolean Lattice ) proof assume A1: L is Boolean Lattice ; ::_thesis: ( L is lower-bounded' & L is upper-bounded' & L is join-commutative & L is meet-commutative & L is distributive & L is distributive' & L is complemented' ) then reconsider L9 = L as Boolean Lattice ; ex c being Element of L9 st for a being Element of L9 holds ( c "\/" a = a & a "\/" c = a ) proof take Bottom L9 ; ::_thesis: for a being Element of L9 holds ( (Bottom L9) "\/" a = a & a "\/" (Bottom L9) = a ) thus for a being Element of L9 holds ( (Bottom L9) "\/" a = a & a "\/" (Bottom L9) = a ) ; ::_thesis: verum end; hence A2: L is lower-bounded' by Def3; ::_thesis: ( L is upper-bounded' & L is join-commutative & L is meet-commutative & L is distributive & L is distributive' & L is complemented' ) ex c being Element of L9 st for a being Element of L9 holds ( c "/\" a = a & a "/\" c = a ) proof take Top L9 ; ::_thesis: for a being Element of L9 holds ( (Top L9) "/\" a = a & a "/\" (Top L9) = a ) thus for a being Element of L9 holds ( (Top L9) "/\" a = a & a "/\" (Top L9) = a ) ; ::_thesis: verum end; hence A3: L is upper-bounded' by Def1; ::_thesis: ( L is join-commutative & L is meet-commutative & L is distributive & L is distributive' & L is complemented' ) thus ( L is join-commutative & L is meet-commutative ) by A1; ::_thesis: ( L is distributive & L is distributive' & L is complemented' ) for a, b, c being Element of L9 holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) by LATTICES:def_11; then for a, b, c being Element of L9 holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) by LATTICES:3; hence ( L is distributive & L is distributive' ) by Def5; ::_thesis: L is complemented' hence L is complemented' by A1, A2, A3, Th24; ::_thesis: verum end; thus ( L is lower-bounded' & L is upper-bounded' & L is join-commutative & L is meet-commutative & L is distributive & L is distributive' & L is complemented' implies L is Boolean Lattice ) ::_thesis: verum proof assume ( L is lower-bounded' & L is upper-bounded' & L is join-commutative & L is meet-commutative & L is distributive & L is distributive' & L is complemented' ) ; ::_thesis: L is Boolean Lattice then reconsider L9 = L as non empty join-commutative meet-commutative distributive join-idempotent upper-bounded' lower-bounded' distributive' complemented' LattStr by Th9; A4: L9 is complemented by Th23; A5: ( L9 is lower-bounded & L9 is upper-bounded ) by Th12, Th14; A6: ( L9 is meet-absorbing & L9 is join-absorbing ) by Th10, Th11; then ( L9 is join-associative & L9 is meet-associative ) by Th16, Th17; hence L is Boolean Lattice by A5, A4, A6; ::_thesis: verum end; end; registration cluster non empty Lattice-like Boolean -> non empty join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' complemented' for LattStr ; coherence for b1 being non empty LattStr st b1 is Boolean & b1 is Lattice-like holds ( b1 is lower-bounded' & b1 is upper-bounded' & b1 is complemented' & b1 is join-commutative & b1 is meet-commutative & b1 is distributive & b1 is distributive' ) by Th25; cluster non empty join-commutative meet-commutative distributive upper-bounded' lower-bounded' distributive' complemented' -> non empty Lattice-like Boolean for LattStr ; coherence for b1 being non empty LattStr st b1 is lower-bounded' & b1 is upper-bounded' & b1 is complemented' & b1 is join-commutative & b1 is meet-commutative & b1 is distributive & b1 is distributive' holds ( b1 is Boolean & b1 is Lattice-like ) by Th25; end; begin definition attrc1 is strict ; struct ShefferStr -> 1-sorted ; aggrShefferStr(# carrier, stroke #) -> ShefferStr ; sel stroke c1 -> BinOp of the carrier of c1; end; definition attrc1 is strict ; struct ShefferLattStr -> ShefferStr , LattStr ; aggrShefferLattStr(# carrier, L_join, L_meet, stroke #) -> ShefferLattStr ; end; definition attrc1 is strict ; struct ShefferOrthoLattStr -> ShefferStr , OrthoLattStr ; aggrShefferOrthoLattStr(# carrier, L_join, L_meet, Compl, stroke #) -> ShefferOrthoLattStr ; end; definition func TrivShefferOrthoLattStr -> ShefferOrthoLattStr equals :: SHEFFER1:def 10 ShefferOrthoLattStr(# 1,op2,op2,op1,op2 #); coherence ShefferOrthoLattStr(# 1,op2,op2,op1,op2 #) is ShefferOrthoLattStr ; end; :: deftheorem defines TrivShefferOrthoLattStr SHEFFER1:def_10_:_ TrivShefferOrthoLattStr = ShefferOrthoLattStr(# 1,op2,op2,op1,op2 #); registration cluster1 -element for ShefferStr ; existence ex b1 being ShefferStr st b1 is 1 -element proof set S = {{}}; set B = the BinOp of {{}}; take ShefferStr(# {{}}, the BinOp of {{}} #) ; ::_thesis: ShefferStr(# {{}}, the BinOp of {{}} #) is 1 -element thus the carrier of ShefferStr(# {{}}, the BinOp of {{}} #) is 1 -element ; :: according to STRUCT_0:def_19 ::_thesis: verum end; cluster1 -element for ShefferLattStr ; existence ex b1 being ShefferLattStr st b1 is 1 -element proof set S = {{}}; set B = the BinOp of {{}}; take ShefferLattStr(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}} #) ; ::_thesis: ShefferLattStr(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}} #) is 1 -element thus the carrier of ShefferLattStr(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}} #) is 1 -element ; :: according to STRUCT_0:def_19 ::_thesis: verum end; cluster1 -element for ShefferOrthoLattStr ; existence ex b1 being ShefferOrthoLattStr st b1 is 1 -element proof set S = {{}}; set B = the BinOp of {{}}; set A = the UnOp of {{}}; take ShefferOrthoLattStr(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the UnOp of {{}}, the BinOp of {{}} #) ; ::_thesis: ShefferOrthoLattStr(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the UnOp of {{}}, the BinOp of {{}} #) is 1 -element thus the carrier of ShefferOrthoLattStr(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the UnOp of {{}}, the BinOp of {{}} #) is 1 -element ; :: according to STRUCT_0:def_19 ::_thesis: verum end; end; definition let L be non empty ShefferStr ; let x, y be Element of L; funcx | y -> Element of L equals :: SHEFFER1:def 11 the stroke of L . (x,y); coherence the stroke of L . (x,y) is Element of L ; end; :: deftheorem defines | SHEFFER1:def_11_:_ for L being non empty ShefferStr for x, y being Element of L holds x | y = the stroke of L . (x,y); definition let L be non empty ShefferOrthoLattStr ; attrL is properly_defined means :Def12: :: SHEFFER1:def 12 ( ( for x being Element of L holds x | x = x ` ) & ( for x, y being Element of L holds x "\/" y = (x | x) | (y | y) ) & ( for x, y being Element of L holds x "/\" y = (x | y) | (x | y) ) & ( for x, y being Element of L holds x | y = (x `) + (y `) ) ); end; :: deftheorem Def12 defines properly_defined SHEFFER1:def_12_:_ for L being non empty ShefferOrthoLattStr holds ( L is properly_defined iff ( ( for x being Element of L holds x | x = x ` ) & ( for x, y being Element of L holds x "\/" y = (x | x) | (y | y) ) & ( for x, y being Element of L holds x "/\" y = (x | y) | (x | y) ) & ( for x, y being Element of L holds x | y = (x `) + (y `) ) ) ); definition let L be non empty ShefferStr ; attrL is satisfying_Sheffer_1 means :Def13: :: SHEFFER1:def 13 for x being Element of L holds (x | x) | (x | x) = x; attrL is satisfying_Sheffer_2 means :Def14: :: SHEFFER1:def 14 for x, y being Element of L holds x | (y | (y | y)) = x | x; attrL is satisfying_Sheffer_3 means :Def15: :: SHEFFER1:def 15 for x, y, z being Element of L holds (x | (y | z)) | (x | (y | z)) = ((y | y) | x) | ((z | z) | x); end; :: deftheorem Def13 defines satisfying_Sheffer_1 SHEFFER1:def_13_:_ for L being non empty ShefferStr holds ( L is satisfying_Sheffer_1 iff for x being Element of L holds (x | x) | (x | x) = x ); :: deftheorem Def14 defines satisfying_Sheffer_2 SHEFFER1:def_14_:_ for L being non empty ShefferStr holds ( L is satisfying_Sheffer_2 iff for x, y being Element of L holds x | (y | (y | y)) = x | x ); :: deftheorem Def15 defines satisfying_Sheffer_3 SHEFFER1:def_15_:_ for L being non empty ShefferStr holds ( L is satisfying_Sheffer_3 iff for x, y, z being Element of L holds (x | (y | z)) | (x | (y | z)) = ((y | y) | x) | ((z | z) | x) ); registration cluster1 -element -> 1 -element satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 for ShefferStr ; coherence for b1 being 1 -element ShefferStr holds ( b1 is satisfying_Sheffer_1 & b1 is satisfying_Sheffer_2 & b1 is satisfying_Sheffer_3 ) proof let L be 1 -element ShefferStr ; ::_thesis: ( L is satisfying_Sheffer_1 & L is satisfying_Sheffer_2 & L is satisfying_Sheffer_3 ) thus L is satisfying_Sheffer_1 ::_thesis: ( L is satisfying_Sheffer_2 & L is satisfying_Sheffer_3 ) proof let x be Element of L; :: according to SHEFFER1:def_13 ::_thesis: (x | x) | (x | x) = x thus (x | x) | (x | x) = x by STRUCT_0:def_10; ::_thesis: verum end; thus L is satisfying_Sheffer_2 ::_thesis: L is satisfying_Sheffer_3 proof let x, y be Element of L; :: according to SHEFFER1:def_14 ::_thesis: x | (y | (y | y)) = x | x thus x | (y | (y | y)) = x | x by STRUCT_0:def_10; ::_thesis: verum end; let x, y, z be Element of L; :: according to SHEFFER1:def_15 ::_thesis: (x | (y | z)) | (x | (y | z)) = ((y | y) | x) | ((z | z) | x) thus (x | (y | z)) | (x | (y | z)) = ((y | y) | x) | ((z | z) | x) by STRUCT_0:def_10; ::_thesis: verum end; end; registration cluster1 -element -> 1 -element join-commutative join-associative for \/-SemiLattStr ; coherence for b1 being 1 -element \/-SemiLattStr holds ( b1 is join-commutative & b1 is join-associative ) proof let L be 1 -element \/-SemiLattStr ; ::_thesis: ( L is join-commutative & L is join-associative ) thus L is join-commutative ::_thesis: L is join-associative proof let x, y be Element of L; :: according to LATTICES:def_4 ::_thesis: x "\/" y = y "\/" x thus x "\/" y = y "\/" x by STRUCT_0:def_10; ::_thesis: verum end; let x, y, z be Element of L; :: according to LATTICES:def_5 ::_thesis: x "\/" (y "\/" z) = (x "\/" y) "\/" z thus x "\/" (y "\/" z) = (x "\/" y) "\/" z by STRUCT_0:def_10; ::_thesis: verum end; cluster1 -element -> 1 -element meet-commutative meet-associative for /\-SemiLattStr ; coherence for b1 being 1 -element /\-SemiLattStr holds ( b1 is meet-commutative & b1 is meet-associative ) proof let L be 1 -element /\-SemiLattStr ; ::_thesis: ( L is meet-commutative & L is meet-associative ) thus L is meet-commutative ::_thesis: L is meet-associative proof let x, y be Element of L; :: according to LATTICES:def_6 ::_thesis: x "/\" y = y "/\" x thus x "/\" y = y "/\" x by STRUCT_0:def_10; ::_thesis: verum end; let x, y, z be Element of L; :: according to LATTICES:def_7 ::_thesis: x "/\" (y "/\" z) = (x "/\" y) "/\" z thus x "/\" (y "/\" z) = (x "/\" y) "/\" z by STRUCT_0:def_10; ::_thesis: verum end; end; registration cluster1 -element -> 1 -element meet-absorbing join-absorbing Boolean for LattStr ; coherence for b1 being 1 -element LattStr holds ( b1 is join-absorbing & b1 is meet-absorbing & b1 is Boolean ) proof let L be 1 -element LattStr ; ::_thesis: ( L is join-absorbing & L is meet-absorbing & L is Boolean ) thus L is join-absorbing ::_thesis: ( L is meet-absorbing & L is Boolean ) proof let x, y be Element of L; :: according to LATTICES:def_9 ::_thesis: x "/\" (x "\/" y) = x thus x "/\" (x "\/" y) = x by STRUCT_0:def_10; ::_thesis: verum end; A1: L is upper-bounded proof set c = the Element of L; take the Element of L ; :: according to LATTICES:def_14 ::_thesis: for b1 being M2( the carrier of L) holds ( the Element of L "\/" b1 = the Element of L & b1 "\/" the Element of L = the Element of L ) let a be Element of L; ::_thesis: ( the Element of L "\/" a = the Element of L & a "\/" the Element of L = the Element of L ) thus ( the Element of L "\/" a = the Element of L & a "\/" the Element of L = the Element of L ) by STRUCT_0:def_10; ::_thesis: verum end; thus L is meet-absorbing ::_thesis: L is Boolean proof let x, y be Element of L; :: according to LATTICES:def_8 ::_thesis: (x "/\" y) "\/" y = y thus (x "/\" y) "\/" y = y by STRUCT_0:def_10; ::_thesis: verum end; A2: L is lower-bounded proof set c = the Element of L; take the Element of L ; :: according to LATTICES:def_13 ::_thesis: for b1 being M2( the carrier of L) holds ( the Element of L "/\" b1 = the Element of L & b1 "/\" the Element of L = the Element of L ) let a be Element of L; ::_thesis: ( the Element of L "/\" a = the Element of L & a "/\" the Element of L = the Element of L ) thus ( the Element of L "/\" a = the Element of L & a "/\" the Element of L = the Element of L ) by STRUCT_0:def_10; ::_thesis: verum end; A3: L is complemented proof set a = the Element of L; let b be Element of L; :: according to LATTICES:def_19 ::_thesis: ex b1 being M2( the carrier of L) st b1 is_a_complement_of b take the Element of L ; ::_thesis: the Element of L is_a_complement_of b A4: ( the Element of L "/\" b = Bottom L & b "/\" the Element of L = Bottom L ) by STRUCT_0:def_10; ( the Element of L "\/" b = Top L & b "\/" the Element of L = Top L ) by STRUCT_0:def_10; hence the Element of L is_a_complement_of b by A4, LATTICES:def_18; ::_thesis: verum end; L is distributive proof let a, b, c be Element of L; :: according to LATTICES:def_11 ::_thesis: a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) thus a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) by STRUCT_0:def_10; ::_thesis: verum end; hence L is Boolean by A2, A1, A3; ::_thesis: verum end; end; registration cluster TrivShefferOrthoLattStr -> 1 -element ; coherence TrivShefferOrthoLattStr is 1 -element by CARD_1:49, STRUCT_0:def_19; cluster TrivShefferOrthoLattStr -> well-complemented properly_defined ; coherence ( TrivShefferOrthoLattStr is properly_defined & TrivShefferOrthoLattStr is well-complemented ) proof set L = TrivShefferOrthoLattStr ; A1: ( ( for x, y being Element of TrivShefferOrthoLattStr holds x "/\" y = (x | y) | (x | y) ) & ( for x, y being Element of TrivShefferOrthoLattStr holds x | y = (x `) + (y `) ) ) by STRUCT_0:def_10; ( ( for x being Element of TrivShefferOrthoLattStr holds x | x = x ` ) & ( for x, y being Element of TrivShefferOrthoLattStr holds x "\/" y = (x | x) | (y | y) ) ) by STRUCT_0:def_10; hence TrivShefferOrthoLattStr is properly_defined by A1, Def12; ::_thesis: TrivShefferOrthoLattStr is well-complemented TrivShefferOrthoLattStr is well-complemented proof let a be Element of TrivShefferOrthoLattStr; :: according to ROBBINS1:def_10 ::_thesis: a ` is_a_complement_of a ( a "\/" (a `) = Top TrivShefferOrthoLattStr & a "/\" (a `) = Bottom TrivShefferOrthoLattStr ) by STRUCT_0:def_10; hence a ` is_a_complement_of a by LATTICES:def_18; ::_thesis: verum end; hence TrivShefferOrthoLattStr is well-complemented ; ::_thesis: verum end; end; registration cluster non empty Lattice-like Boolean well-complemented properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 for ShefferOrthoLattStr ; existence ex b1 being non empty ShefferOrthoLattStr st ( b1 is properly_defined & b1 is Boolean & b1 is well-complemented & b1 is Lattice-like & b1 is satisfying_Sheffer_1 & b1 is satisfying_Sheffer_2 & b1 is satisfying_Sheffer_3 ) proof take TrivShefferOrthoLattStr ; ::_thesis: ( TrivShefferOrthoLattStr is properly_defined & TrivShefferOrthoLattStr is Boolean & TrivShefferOrthoLattStr is well-complemented & TrivShefferOrthoLattStr is Lattice-like & TrivShefferOrthoLattStr is satisfying_Sheffer_1 & TrivShefferOrthoLattStr is satisfying_Sheffer_2 & TrivShefferOrthoLattStr is satisfying_Sheffer_3 ) thus ( TrivShefferOrthoLattStr is properly_defined & TrivShefferOrthoLattStr is Boolean & TrivShefferOrthoLattStr is well-complemented & TrivShefferOrthoLattStr is Lattice-like & TrivShefferOrthoLattStr is satisfying_Sheffer_1 & TrivShefferOrthoLattStr is satisfying_Sheffer_2 & TrivShefferOrthoLattStr is satisfying_Sheffer_3 ) ; ::_thesis: verum end; end; theorem :: SHEFFER1:26 for L being non empty Lattice-like Boolean well-complemented properly_defined ShefferOrthoLattStr holds L is satisfying_Sheffer_1 proof 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 end; theorem :: SHEFFER1:27 for L being non empty Lattice-like Boolean well-complemented properly_defined ShefferOrthoLattStr holds L is satisfying_Sheffer_2 proof 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 end; theorem :: SHEFFER1:28 for L being non empty Lattice-like Boolean well-complemented properly_defined ShefferOrthoLattStr holds L is satisfying_Sheffer_3 proof let L be non empty Lattice-like Boolean well-complemented properly_defined ShefferOrthoLattStr ; ::_thesis: L is satisfying_Sheffer_3 let x, y, z be Element of L; :: according to SHEFFER1:def_15 ::_thesis: (x | (y | z)) | (x | (y | z)) = ((y | y) | x) | ((z | z) | x) x *' ((y `) + (z `)) = ((y `) *' x) + ((z `) *' x) by ROBBINS1:30; then ((x `) + ((y | z) `)) ` = ((y `) *' x) + ((z `) *' x) by Def12; then (x | (y | z)) ` = ((y `) *' x) + ((z `) *' x) by Def12; then (x | (y | z)) | (x | (y | z)) = ((y `) *' x) + ((z `) *' x) by Def12 .= ((y `) *' ((x `) `)) + ((z `) *' x) by ROBBINS1:3 .= ((y `) *' ((x `) `)) + ((z `) *' ((x `) `)) by ROBBINS1:3 .= ((y + (x `)) `) + ((z `) *' ((x `) `)) by Th1 .= ((y + (x `)) `) + ((z + (x `)) `) by Th1 .= (y + (x `)) | (z + (x `)) by Def12 .= (((y `) `) + (x `)) | (z + (x `)) by ROBBINS1:3 .= (((y `) `) + (x `)) | (((z `) `) + (x `)) by ROBBINS1:3 .= ((y `) | x) | (((z `) `) + (x `)) by Def12 .= ((y `) | x) | ((z `) | x) by Def12 .= ((y | y) | x) | ((z `) | x) by Def12 .= ((y | y) | x) | ((z | z) | x) by Def12 ; hence (x | (y | z)) | (x | (y | z)) = ((y | y) | x) | ((z | z) | x) ; ::_thesis: verum end; definition let L be non empty ShefferStr ; let a be Element of L; funca " -> Element of L equals :: SHEFFER1:def 16 a | a; coherence a | a is Element of L ; end; :: deftheorem defines " SHEFFER1:def_16_:_ for L being non empty ShefferStr for a being Element of L holds a " = a | a; theorem :: SHEFFER1:29 for L being non empty satisfying_Sheffer_3 ShefferOrthoLattStr for x, y, z being Element of L holds (x | (y | z)) " = ((y ") | x) | ((z ") | x) by Def15; theorem :: SHEFFER1:30 for L being non empty satisfying_Sheffer_1 ShefferOrthoLattStr for x being Element of L holds x = (x ") " by Def13; theorem Th31: :: SHEFFER1:31 for L being non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr for x, y being Element of L holds x | y = y | x proof let L be non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr ; ::_thesis: for x, y being Element of L holds x | y = y | x let x, y be Element of L; ::_thesis: x | y = y | x x | y = ((x | y) ") " by Def13 .= ((x | ((y ") ")) ") " by Def13 .= ((((y ") ") | x) ") " by Def15 .= ((y | x) ") " by Def13 .= y | x by Def13 ; hence x | y = y | x ; ::_thesis: verum end; theorem Th32: :: SHEFFER1:32 for L being non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr for x, y being Element of L holds x | (x | x) = y | (y | y) proof let L be non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr ; ::_thesis: for x, y being Element of L holds x | (x | x) = y | (y | y) let x, y be Element of L; ::_thesis: x | (x | x) = y | (y | y) x | (x | x) = ((x | (x ")) | (x | (x "))) " by Def13 .= ((x | (x ")) | (y | (y "))) " by Def14 .= ((y | (y ")) | (x | (x | x))) " by Th31 .= ((y | (y ")) ") " by Def14 .= y | (y | y) by Def13 ; hence x | (x | x) = y | (y | y) ; ::_thesis: verum end; theorem Th33: :: SHEFFER1:33 for L being non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr holds L is join-commutative proof let L be non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr ; ::_thesis: L is join-commutative let x, y be Element of L; :: according to LATTICES:def_4 ::_thesis: x "\/" y = y "\/" x x "\/" y = (x ") | (y | y) by Def12 .= (y | y) | (x | x) by Th31 .= y "\/" x by Def12 ; hence x "\/" y = y "\/" x ; ::_thesis: verum end; theorem Th34: :: SHEFFER1:34 for L being non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr holds L is meet-commutative proof let L be non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr ; ::_thesis: L is meet-commutative let x, y be Element of L; :: according to LATTICES:def_6 ::_thesis: x "/\" y = y "/\" x x "/\" y = (x | y) | (x | y) by Def12 .= (y | x) | (x | y) by Th31 .= (y | x) | (y | x) by Th31 .= y "/\" x by Def12 ; hence x "/\" y = y "/\" x ; ::_thesis: verum end; theorem Th35: :: SHEFFER1:35 for L being non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr holds L is distributive proof let L be non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr ; ::_thesis: L is distributive let x, y, z be Element of L; :: according to LATTICES:def_11 ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) set Y = y " ; set Z = z " ; x "/\" (y "\/" z) = x "/\" ((y | y) | (z | z)) by Def12 .= (x | ((y ") | (z "))) " by Def12 .= (((y ") ") | x) | (((z ") ") | x) by Def15 .= (y | x) | (((z ") ") | x) by Def13 .= (y | x) | (z | x) by Def13 .= (x | y) | (z | x) by Th31 .= (x | y) | (x | z) by Th31 .= (((x | y) ") ") | (x | z) by Def13 .= (((x | y) | (x | y)) ") | (((x | z) ") ") by Def13 .= ((x "/\" y) | ((x | y) | (x | y))) | (((x | z) | (x | z)) | ((x | z) | (x | z))) by Def12 .= ((x "/\" y) | (x "/\" y)) | (((x | z) | (x | z)) | ((x | z) | (x | z))) by Def12 .= ((x "/\" y) | (x "/\" y)) | ((x "/\" z) | ((x | z) | (x | z))) by Def12 .= ((x "/\" y) | (x "/\" y)) | ((x "/\" z) | (x "/\" z)) by Def12 .= (x "/\" y) "\/" (x "/\" z) by Def12 ; hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) ; ::_thesis: verum end; theorem Th36: :: SHEFFER1:36 for L being non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr holds L is distributive' proof let L be non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr ; ::_thesis: L is distributive' let x, y, z be Element of L; :: according to SHEFFER1:def_5 ::_thesis: x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z) set X = x | x; x "\/" (y "/\" z) = x "\/" ((y | z) | (y | z)) by Def12 .= (x | x) | (((y | z) ") ") by Def12 .= (x | x) | (y | z) by Def13 .= (((x | x) | (y | z)) ") " by Def13 .= (((y ") | (x | x)) | ((z ") | (x | x))) " by Def15 .= (((x | x) | (y ")) | ((z ") | (x | x))) " by Th31 .= (((x | x) | (y | y)) | ((x | x) | (z "))) " by Th31 .= ((x "\/" y) | ((x | x) | (z | z))) | (((x | x) | (y | y)) | ((x | x) | (z | z))) by Def12 .= ((x "\/" y) | (x "\/" z)) | (((x | x) | (y | y)) | ((x | x) | (z | z))) by Def12 .= ((x "\/" y) | (x "\/" z)) | ((x "\/" y) | ((x | x) | (z | z))) by Def12 .= ((x "\/" y) | (x "\/" z)) | ((x "\/" y) | (x "\/" z)) by Def12 .= (x "\/" y) "/\" (x "\/" z) by Def12 ; hence x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z) ; ::_thesis: verum end; theorem :: SHEFFER1:37 for L being non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr holds L is Boolean Lattice proof let L be non empty properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferOrthoLattStr ; ::_thesis: L is Boolean Lattice A1: ( L is distributive & L is distributive' ) by Th35, Th36; ex c being Element of L st for a being Element of L holds ( c "/\" a = a & a "/\" c = a ) proof set b = the Element of L; take c = ( the Element of L | the Element of L) | (( the Element of L | the Element of L) | ( the Element of L | the Element of L)); ::_thesis: for a being Element of L holds ( c "/\" a = a & a "/\" c = a ) let a be Element of L; ::_thesis: ( c "/\" a = a & a "/\" c = a ) thus c "/\" a = a ::_thesis: a "/\" c = a proof set X = the Element of L " ; c "/\" a = ((( the Element of L | the Element of L) | (( the Element of L ") | ( the Element of L "))) | a) " by Def12 .= (a | (( the Element of L ") | (( the Element of L ") | ( the Element of L ")))) " by Th31 .= (a | a) " by Def14 .= a by Def13 ; hence c "/\" a = a ; ::_thesis: verum end; thus a "/\" c = a ::_thesis: verum proof set X = the Element of L " ; a "/\" c = (a | (( the Element of L | the Element of L) | (( the Element of L ") | ( the Element of L ")))) " by Def12 .= (a | a) " by Def14 .= a by Def13 ; hence a "/\" c = a ; ::_thesis: verum end; end; then A2: L is upper-bounded' by Def1; ex c being Element of L st for a being Element of L holds ( c "\/" a = a & a "\/" c = a ) proof set b = the Element of L; take c = ( the Element of L | ( the Element of L | the Element of L)) | ( the Element of L | ( the Element of L | the Element of L)); ::_thesis: for a being Element of L holds ( c "\/" a = a & a "\/" c = a ) let a be Element of L; ::_thesis: ( c "\/" a = a & a "\/" c = a ) c "\/" a = ((( the Element of L | ( the Element of L | the Element of L)) ") ") | (a | a) by Def12 .= (((a | (a | a)) ") ") | (a | a) by Th32 .= (a | (a | a)) | (a | a) by Def13 .= (a | a) | (a | (a | a)) by Th31 .= (a | a) | (a | a) by Def14 .= a by Def13 ; hence c "\/" a = a ; ::_thesis: a "\/" c = a a "\/" c = (a | a) | ((( the Element of L | ( the Element of L | the Element of L)) ") ") by Def12 .= (a | a) | (((a | (a | a)) ") ") by Th32 .= (a | a) | (a | (a | a)) by Def13 .= (a | a) | (a | a) by Def14 .= a by Def13 ; hence a "\/" c = a ; ::_thesis: verum end; then A3: L is lower-bounded' by Def3; for b being Element of L ex a being Element of L st a is_a_complement'_of b proof let b be Element of L; ::_thesis: ex a being Element of L st a is_a_complement'_of b set a = b | b; take b | b ; ::_thesis: b | b is_a_complement'_of b A4: Top' L = (b | b) | ((b | b) | (b | b)) proof set X = (b | b) | ((b | b) | (b | b)); for a being Element of L holds ( ((b | b) | ((b | b) | (b | b))) "/\" a = a & a "/\" ((b | b) | ((b | b) | (b | b))) = a ) proof let a be Element of L; ::_thesis: ( ((b | b) | ((b | b) | (b | b))) "/\" a = a & a "/\" ((b | b) | ((b | b) | (b | b))) = a ) set Y = b " ; thus ((b | b) | ((b | b) | (b | b))) "/\" a = (((b | b) | ((b ") | (b "))) | a) " by Def12 .= (a | ((b ") | ((b ") | (b ")))) " by Th31 .= (a | a) " by Def14 .= a by Def13 ; ::_thesis: a "/\" ((b | b) | ((b | b) | (b | b))) = a thus a "/\" ((b | b) | ((b | b) | (b | b))) = (a | ((b | b) | ((b ") | (b ")))) " by Def12 .= (a | a) " by Def14 .= a by Def13 ; ::_thesis: verum end; hence Top' L = (b | b) | ((b | b) | (b | b)) by A2, Def2; ::_thesis: verum end; then A5: b "\/" (b | b) = Top' L by Def12; A6: Bot' L = (b | (b | b)) | (b | (b | b)) proof set X = (b | (b | b)) | (b | (b | b)); for a being Element of L holds ( ((b | (b | b)) | (b | (b | b))) "\/" a = a & a "\/" ((b | (b | b)) | (b | (b | b))) = a ) proof let a be Element of L; ::_thesis: ( ((b | (b | b)) | (b | (b | b))) "\/" a = a & a "\/" ((b | (b | b)) | (b | (b | b))) = a ) thus ((b | (b | b)) | (b | (b | b))) "\/" a = (((b | (b | b)) ") ") | (a | a) by Def12 .= (((a | (a | a)) ") ") | (a | a) by Th32 .= (a | (a | a)) | (a | a) by Def13 .= (a | a) | (a | (a | a)) by Th31 .= (a | a) | (a | a) by Def14 .= a by Def13 ; ::_thesis: a "\/" ((b | (b | b)) | (b | (b | b))) = a thus a "\/" ((b | (b | b)) | (b | (b | b))) = (a | a) | (((b | (b | b)) ") ") by Def12 .= (a | a) | (((a | (a | a)) ") ") by Th32 .= (a | a) | (a | (a | a)) by Def13 .= (a | a) | (a | a) by Def14 .= a by Def13 ; ::_thesis: verum end; hence Bot' L = (b | (b | b)) | (b | (b | b)) by A3, Def4; ::_thesis: verum end; then A7: b "/\" (b | b) = Bot' L by Def12; A8: (b | b) "\/" b = ((b | b) | (b | b)) | (b | b) by Def12 .= Top' L by A4, Th31 ; (b | b) "/\" b = ((b | b) | b) | ((b | b) | b) by Def12 .= (b | (b | b)) | ((b | b) | b) by Th31 .= Bot' L by A6, Th31 ; hence b | b is_a_complement'_of b by A8, A5, A7, Def6; ::_thesis: verum end; then A9: L is complemented' by Def7; ( L is join-commutative & L is meet-commutative ) by Th33, Th34; hence L is Boolean Lattice by A3, A2, A9, A1; ::_thesis: verum end;