let X be set ; :: thesis: for Y being ext-real-membered set st X c= Y holds
X is ext-real-membered
let Y be ext-real-membered set ; :: thesis: ( X c= Y implies X is ext-real-membered )
assume A1: X c= Y ; :: thesis: X is ext-real-membered
let x be set ; :: according to MEMBERED:def 2 :: thesis: ( x in X implies x is ext-real )
thus ( x in X implies x is ext-real ) by A1; :: thesis: verum