let
T
be
Ternary_Boolean_Algebra
;
:: thesis:
for
a
being
Element
of
T
holds
(
a
`
)
`
=
a
let
a
be
Element
of
T
;
:: thesis:
(
a
`
)
`
=
a
a
=
Tern
(
(
(
a
`
)
`
)
,
(
a
`
)
,
a
)
by
TLADef
.=
(
a
`
)
`
by
Lemma34
;
hence
(
a
`
)
`
=
a
;
:: thesis:
verum