consider L being non empty trivial Lattice;
A1: L is lower-bounded

proof

consider x being Element of L;
for y being Element of L holds
( x "/\" y = x & y "/\" x = x ) by STRUCT_0:def 10;
hence L is lower-bounded by LATTICES:def 13; :: thesis: verum

end;

A2: L is upper-bounded

proof

consider x being Element of L;
for y being Element of L holds
( x "\/" y = x & y "\/" x = x ) by STRUCT_0:def 10;
hence L is upper-bounded by LATTICES:def 14; :: thesis: verum

end;

for b being Element of L ex a being Element of L st a is_a_complement_of b

proof

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

end;

then A3: L is complemented by LATTICES:def 19;
A4: L is join-idempotent

proof

let x be Element of L; :: 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 L ex a being Element of L st a is_a_complement'_of b

proof

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

end;

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

proof

consider x being Element of L;
for y being Element of L holds
( x "\/" y = y & y "\/" x = y ) by STRUCT_0:def 10;
hence L is lower-bounded' by Def3; :: thesis: verum

end;

A8: L is upper-bounded'

proof

consider x being Element of L;
for y being Element of L holds
( x "/\" y = y & y "/\" x = y ) by STRUCT_0:def 10;
hence L is upper-bounded' by Def1; :: thesis: verum

end;

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