take
F
=
F_Real
;
:: thesis:
F
is
Fanoian
let
a
be
Element
of
F
;
:: according to
VECTSP_1:def 17
:: thesis:
(
a
+
a
=
0.
F
implies
a
=
0.
F
)
assume
A1
:
a
+
a
=
0.
F
;
:: thesis:
a
=
0.
F
a
=
(
1.
F
)
*
a
;
then
a
+
a
=
(
(
1.
F
)
+
(
1.
F
)
)
*
a
by
Def7
;
hence
a
=
0.
F
by
A1
,
Th8
,
Th22
;
:: thesis:
verum