let E be set ; :: thesis: for x being object st <%x%> is Element of E ^omega holds
x in E
let x be object ; :: thesis: ( <%x%> is Element of E ^omega implies x in E )
assume <%x%> is Element of E ^omega ; :: thesis: x in E
then rng <%x%> c= E by RELAT_1:def 19;
then {x} c= E by AFINSQ_1:33;
hence x in E by ZFMISC_1:31; :: thesis: verum