let
Y
be non
empty
TopStruct
;
:: thesis:
for
x
being
Point
of
Y
holds
{
x
}
c=
union
(
MaxADSF
x
)
let
x
be
Point
of
Y
;
:: thesis:
{
x
}
c=
union
(
MaxADSF
x
)
{
x
}
=
meet
(
MaxADSF
x
)
by
Th11
;
hence
{
x
}
c=
union
(
MaxADSF
x
)
by
SETFAM_1:2
;
:: thesis:
verum