let
a
,
b
be
Element
of
AS
;
:: thesis:
Line
(
a
,
b
)
=
Line
(
b
,
a
)
A1
:
Line
(
b
,
a
)
c=
Line
(
a
,
b
)
by
Lm5
;
Line
(
a
,
b
)
c=
Line
(
b
,
a
)
by
Lm5
;
hence
Line
(
a
,
b
)
=
Line
(
b
,
a
)
by
A1
,
XBOOLE_0:def 10
;
:: thesis:
verum