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

x
)

(
y

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

x
)

(
y

x
)
=
x
set
Y
=
y

x
;
x

(
(
(
(
y

x
)

(
y

x
)
)

x
)

x
)
=
y

x
by
Th10
;
hence
(
x

x
)

(
y

x
)
=
x
by
Th7
;
:: thesis:
verum