set L = TrivOrtLat ;
thus TrivOrtLat is bounded ; :: according to LATTICES:def 20 :: 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 b1 being M3( the carrier of TrivOrtLat) st b1 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 ; :: thesis: verum
end;
thus TrivOrtLat is distributive by STRUCT_0:def 10; :: thesis: TrivOrtLat is well-complemented
let a be Element of TrivOrtLat; :: according to ROBBINS1:def 10 :: thesis: a ` is_a_complement_of a
A1: ( (a `) "\/" a = a "\/" (a `) & (a `) "/\" a = a "/\" (a `) ) ;
( (a `) "\/" a = Top TrivOrtLat & (a `) "/\" a = Bottom TrivOrtLat ) by STRUCT_0:def 10;
hence a ` is_a_complement_of a by A1; :: thesis: verum