let
X
be
set
;
:: thesis:
bspace
X
is
Abelian
let
x
,
y
be
Element
of
(
bspace
X
)
;
:: according to
RLVECT_1:def 2
:: thesis:
x
+
y
=
y
+
x
reconsider
A
=
x
,
B
=
y
as
Subset
of
X
;
x
+
y
=
B
\+\
A
by
Def5
.=
y
+
x
by
Def5
;
hence
x
+
y
=
y
+
x
;
:: thesis:
verum