let e be Element of X; :: thesis: e is ext-real

per cases ( X is empty or not X is empty ) ;

suppose X is empty ; :: thesis: e is ext-real

hence e is ext-real by SUBSET_1:def 1; :: thesis: verum

end;

suppose not X is empty ; :: thesis: e is ext-real

hence e is ext-real by Def2; :: thesis: verum

end;

end;