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 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 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 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