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 ; :: 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 ; :: 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 ; :: thesis: verum

end;

then A3: the 1 -element Lattice is complemented ;
A4: the 1 -element Lattice is join-idempotent ;
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 ; :: thesis: verum

end;

then A5: the 1 -element Lattice is complemented' ;
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 ;
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' ; :: 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' ; :: 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' ;
hence ex b₁ being 1 -element LattStr st
( b₁ is Boolean & b₁ is join-idempotent & b₁ is upper-bounded' & b₁ is complemented' & b₁ is distributive' & b₁ is lower-bounded' & b₁ is Lattice-like ) by A3, A6, A1, A2, A4, A8, A5, A7; :: thesis: verum