set L = the non empty trivial Lattice;
A1: the non empty trivial Lattice is lower-bounded

proof

set x = the Element of the non empty trivial Lattice;
for y being Element of the non empty trivial Lattice holds
( the Element of the non empty trivial Lattice "/\" y = the Element of the non empty trivial Lattice & y "/\" the Element of the non empty trivial Lattice = the Element of the non empty trivial Lattice ) by STRUCT_0:def 10;
hence the non empty trivial Lattice is lower-bounded by LATTICES:def 13; :: thesis: verum

end;

A2: the non empty trivial Lattice is upper-bounded

proof

set x = the Element of the non empty trivial Lattice;
for y being Element of the non empty trivial Lattice holds
( the Element of the non empty trivial Lattice "\/" y = the Element of the non empty trivial Lattice & y "\/" the Element of the non empty trivial Lattice = the Element of the non empty trivial Lattice ) by STRUCT_0:def 10;
hence the non empty trivial Lattice is upper-bounded by LATTICES:def 14; :: thesis: verum

end;

for b being Element of the non empty trivial Lattice ex a being Element of the non empty trivial Lattice st a is_a_complement_of b

proof

let b be Element of the non empty trivial Lattice; :: thesis: ex a being Element of the non empty trivial Lattice st a is_a_complement_of b
take a = b; :: thesis: a is_a_complement_of b
( b "\/" a = Top the non empty trivial Lattice & b "/\" a = Bottom the non empty trivial Lattice ) by STRUCT_0:def 10;
hence a is_a_complement_of b by LATTICES:def 18; :: thesis: verum

end;

then A3: the non empty trivial Lattice is complemented by LATTICES:def 19;
A4: the non empty trivial Lattice is join-idempotent

proof

let x be Element of the non empty trivial Lattice; :: according to ROBBINS1:def 7 :: thesis: x "\/" x = x
thus x "\/" x = x by STRUCT_0:def 10; :: thesis: verum

end;

for b being Element of the non empty trivial Lattice ex a being Element of the non empty trivial Lattice st a is_a_complement'_of b

proof

let b be Element of the non empty trivial Lattice; :: thesis: ex a being Element of the non empty trivial Lattice st a is_a_complement'_of b
take a = b; :: thesis: a is_a_complement'_of b
( b "\/" a = Top' the non empty trivial Lattice & b "/\" a = Bot' the non empty trivial Lattice ) by STRUCT_0:def 10;
hence a is_a_complement'_of b by Def6; :: thesis: verum

end;

then A5: the non empty trivial Lattice is complemented' by Def7;
for a, b, c being Element of the non empty trivial Lattice holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) by STRUCT_0:def 10;
then A6: the non empty trivial Lattice is distributive by LATTICES:def 11;
A7: the non empty trivial Lattice is lower-bounded'

proof

set x = the Element of the non empty trivial Lattice;
for y being Element of the non empty trivial Lattice holds
( the Element of the non empty trivial Lattice "\/" y = y & y "\/" the Element of the non empty trivial Lattice = y ) by STRUCT_0:def 10;
hence the non empty trivial Lattice is lower-bounded' by Def3; :: thesis: verum

end;

A8: the non empty trivial Lattice is upper-bounded'

proof

set x = the Element of the non empty trivial Lattice;
for y being Element of the non empty trivial Lattice holds
( the Element of the non empty trivial Lattice "/\" y = y & y "/\" the Element of the non empty trivial Lattice = y ) by STRUCT_0:def 10;
hence the non empty trivial Lattice is upper-bounded' by Def1; :: thesis: verum

end;

for a, b, c being Element of the non empty trivial Lattice holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) by STRUCT_0:def 10;
then the non empty trivial Lattice is distributive' by Def5;
hence ex b₁ being non empty 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