set L = TrivOrtLat ;
thus for x, y being Element of TrivOrtLat holds x "/\" y = y "/\" x by STRUCT_0:def 10; :: according to LATTICES:def 6 :: thesis: ( TrivOrtLat is meet-associative & TrivOrtLat is meet-absorbing & TrivOrtLat is join-absorbing )
thus for x, y, z being Element of TrivOrtLat holds (x "/\" y) "/\" z = x "/\" (y "/\" z) by STRUCT_0:def 10; :: according to LATTICES:def 7 :: thesis: ( TrivOrtLat is meet-absorbing & TrivOrtLat is join-absorbing )
thus for x, y being Element of TrivOrtLat holds (x "/\" y) "\/" y = y by STRUCT_0:def 10; :: according to LATTICES:def 8 :: thesis: TrivOrtLat is join-absorbing
let x, y be Element of TrivOrtLat; :: according to LATTICES:def 9 :: thesis: x "/\" (x + y) = x
thus x "/\" (x "\/" y) = x by STRUCT_0:def 10; :: thesis: verum