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

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

hence
TrivShefferOrthoLattStr is well-complemented
; :: thesis: verum
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;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