consider
x
being
object
such that
A1
:
x
in
X
.
s
by
XBOOLE_0:def 1
;
ex
a
being
set
st
(
a
in
X
.
s
&
root-tree
[
x
,
s
]
=
root-tree
[
a
,
s
]
)
by
A1
;
hence
not
FreeGen
(
s
,
X
) is
empty
by
Def15
;
:: thesis:
verum