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

(
y

z
)
)

(
x

z
)
=
x
let
x
,
y
,
z
be
Element
of
L
;
:: thesis:
(
x

(
y

z
)
)

(
x

z
)
=
x
(
z

z
)

(
y

z
)
=
z
by
Th11
;
hence
(
x

(
y

z
)
)

(
x

z
)
=
x
by
Th15
;
:: thesis:
verum