set L = TrivShefferOrthoLattStr ;
A1: ( ( for x, y being Element of TrivShefferOrthoLattStr holds x "/\" y = (x | y) | (x | y) ) & ( for x, y being Element of TrivShefferOrthoLattStr holds x | y = (x `) + (y `) ) ) by STRUCT_0:def 10;
( ( for x being Element of TrivShefferOrthoLattStr holds x | x = x ` ) & ( for x, y being Element of TrivShefferOrthoLattStr holds x "\/" y = (x | x) | (y | y) ) ) by STRUCT_0:def 10;
hence TrivShefferOrthoLattStr is properly_defined by A1; :: thesis: TrivShefferOrthoLattStr is well-complemented
TrivShefferOrthoLattStr is well-complemented

proof

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

end;

hence TrivShefferOrthoLattStr is well-complemented ; :: thesis: verum