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;