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
X
=
x
;
set
Y
=
y
;
y

(
x

y
)
=
(
x

y
)

y
by
Th20
;
hence
(
x

y
)

y
=
y

(
x

x
)
by
Th42
;
:: thesis:
verum