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' ; :: 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' ; :: 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' ) ; :: 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;