let S be Element of X; :: thesis: S is real-membered

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

suppose not X is empty ; :: thesis: S is real-membered

then S in X ;
then S in bool REAL ;
then S c= REAL ;
hence S is real-membered ; :: thesis: verum

end;

suppose X is empty ; :: thesis: S is real-membered

then S = {} by SUBSET_1:def 1;
then S c= REAL ;
hence S is real-membered ; :: thesis: verum

end;

end;