set L = TrivOrtLat ;
thus TrivOrtLat is lower-bounded ; :: according to LATTICES:def 15,LATTICES:def 20 :: thesis: ( TrivOrtLat is upper-bounded & TrivOrtLat is complemented & TrivOrtLat is distributive & TrivOrtLat is well-complemented )
thus TrivOrtLat is upper-bounded ; :: thesis: ( TrivOrtLat is complemented & TrivOrtLat is distributive & TrivOrtLat is well-complemented )
thus TrivOrtLat is complemented :: thesis: ( TrivOrtLat is distributive & TrivOrtLat is well-complemented )

proof

let b be Element of TrivOrtLat; :: according to LATTICES:def 19 :: thesis: ex b₁ being M2( the carrier of TrivOrtLat) st b₁ is_a_complement_of b
take a = b; :: thesis: a is_a_complement_of b
( a "\/" b = Top TrivOrtLat & a "/\" b = Bottom TrivOrtLat ) by STRUCT_0:def 10;
hence a is_a_complement_of b by LATTICES:def 18; :: thesis: verum

end;

thus TrivOrtLat is distributive :: thesis: TrivOrtLat is well-complemented

proof

let x, y, z be Element of TrivOrtLat; :: according to LATTICES:def 11 :: thesis: x "/\" (y + z) = (x "/\" y) + (x "/\" z)
thus x "/\" (y + z) = (x "/\" y) + (x "/\" z) by STRUCT_0:def 10; :: thesis: verum

end;

thus TrivOrtLat is well-complemented :: thesis: verum

proof

let a be Element of TrivOrtLat; :: according to ROBBINS1:def 10 :: thesis: a ` is_a_complement_of a
( (a `) "\/" a = Top TrivOrtLat & (a `) "/\" a = Bottom TrivOrtLat ) by STRUCT_0:def 10;
hence a ` is_a_complement_of a by LATTICES:def 18; :: thesis: verum

end;