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