A
=
the
empty
convex
Subset
of
RLS
;
then
A
in
Convex-Family
A
by
CONVEX1:def 4
;
hence
conv
A
is
empty
by
SETFAM_1:4
;
:: thesis:
verum