let
L
be non
empty
satisfying_Sh_1
ShefferStr
;
:: thesis:
for
x
,
y
being
Element
of
L
holds
x

(
y

(
y

y
)
)
=
x

x
let
x
,
y
be
Element
of
L
;
:: thesis:
x

(
y

(
y

y
)
)
=
x

x
set
Y
=
y

(
x

y
)
;
(
y

(
x

y
)
)

(
x

y
)
=
y
by
Th25
;
hence
x

(
y

(
y

y
)
)
=
x

x
by
Th58
;
:: thesis:
verum