thus TrivOrtLat is involutive :: thesis: TrivOrtLat is with_Top

proof

let x be Element of TrivOrtLat; :: according to ROBBINS3:def 6 :: thesis: (x `) ` = x
thus (x `) ` = x by STRUCT_0:def 10; :: thesis: verum

end;

thus TrivOrtLat is with_Top :: thesis: verum

proof

let x, y be Element of TrivOrtLat; :: according to ROBBINS3:def 7 :: thesis: x |_| (x `) = y |_| (y `)
thus x |_| (x `) = y |_| (y `) by STRUCT_0:def 10; :: thesis: verum

end;