defpred
S
_{1}
[
Element
of
FT
]
means
( $1
in
A
&
(
U_FT
$1
)
\
{
$1
}
misses
A
);
{
x
where
x
is
Element
of
FT
:
S
_{1}
[
x
] } is
Subset
of
FT
from
DOMAIN_1:sch 7
();
hence
{
x
where
x
is
Element
of
FT
: (
x
in
A
&
(
U_FT
x
)
\
{
x
}
misses
A
) } is
Subset
of
FT
;
:: thesis:
verum