let
X
be
Element
of
Fin
ExtREAL
;
:: thesis:
X
is
ext-real-membered
X
c=
ExtREAL
by
FINSUB_1:def 5
;
hence
X
is
ext-real-membered
;
:: thesis:
verum