set L = the 1 -element Lattice;

A1: the 1 -element Lattice is lower-bounded

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

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'

then the 1 -element Lattice is distributive' ;

hence ex b_{1} being 1 -element LattStr st

( b_{1} is Boolean & b_{1} is join-idempotent & b_{1} is upper-bounded' & b_{1} is complemented' & b_{1} is distributive' & b_{1} is lower-bounded' & b_{1} is Lattice-like )
by A3, A6, A1, A2, A4, A8, A5, A7; :: thesis: verum

A1: the 1 -element Lattice is lower-bounded

proof

A2:
the 1 -element Lattice is upper-bounded
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;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

proof

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

proof

then A3:
the 1 -element Lattice is complemented
;
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;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

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

then A5:
the 1 -element Lattice is complemented'
;
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;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

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

A8:
the 1 -element Lattice is upper-bounded'
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;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

proof

for a, b, c being Element of the 1 -element Lattice holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c)
by STRUCT_0:def 10;
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 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

then the 1 -element Lattice is distributive' ;

hence ex b

( b