for
x
,
y
being
Element
of
BCI-EXAMPLE
holds
Polynom
(
0
,
0
,
x
,
y
)
=
Polynom
(
0
,
0
,
y
,
x
)
by
STRUCT_0:def 10
;
hence
BCI-EXAMPLE
is
quasi-commutative
;
:: thesis:
verum