let X be set ; :: thesis: ( X is ext-natural-membered implies X is ext-real-membered )
assume A1: X is ext-natural-membered ; :: thesis: X is ext-real-membered

now :: thesis: for x being object st x in X holds
x is ext-real

let x be object ; :: thesis: ( x in X implies x is ext-real )
assume x in X ; :: thesis: x is ext-real
then x is ext-natural by A1;
hence x is ext-real ; :: thesis: verum

end;

hence X is ext-real-membered by MEMBERED:def 2; :: thesis: verum