let
L
be non
empty
satisfying_DN_1
ComplLLattStr
;
:: thesis:
for
x
being
Element
of
L
holds
(
x
`
)
`
=
x
let
x
be
Element
of
L
;
:: thesis:
(
x
`
)
`
=
x
(
x
`
)
`
=
(
(
(
(
(
x
+
(
x
`
)
)
`
)
+
x
)
`
)
+
(
x
`
)
)
`
by
Th22
.=
x
by
Th19
;
hence
(
x
`
)
`
=
x
;
:: thesis:
verum