[(In (x,ExtREAL)),(In (y,ExtREAL))] in [:ExtREAL,ExtREAL:] by ZFMISC_1:87;
hence In ([x,y],[:ExtREAL,ExtREAL:]) = [x,y] by SUBSET_1:def 8; :: thesis: verum