A1
:
field
(
RelIncl
X
)
=
X
by
Def1
;
let
a
be
object
;
:: according to
RELAT_2:def 1
,
RELAT_2:def 9
:: thesis:
( not
a
in
field
(
RelIncl
X
)
or
[
a
,
a
]
in
RelIncl
X
)
assume
a
in
field
(
RelIncl
X
)
;
:: thesis:
[
a
,
a
]
in
RelIncl
X
hence
[
a
,
a
]
in
RelIncl
X
by
A1
,
Def1
;
:: thesis:
verum