set I = {1,2,3};
A1: {1,2,3} = {1,2} \/ {3} by ENUMSET1:3;
( 1 in REAL & 2 in REAL & 3 in REAL ) by NUMBERS:19;
then ( {1,2} c= REAL & {3} c= REAL ) by ZFMISC_1:32;
hence {1,2,3} is non empty Subset of REAL by A1, XBOOLE_1:8; :: thesis: verum