let E be set ; :: thesis: for X being Subset of E
for x being object st x in X holds
x in E
let X be Subset of E; :: thesis: for x being object st x in X holds
x in E
let x be object ; :: thesis: ( x in X implies x in E )
assume A1: x in X ; :: thesis: x in E
X in bool E by Def1;
then X c= E by ZFMISC_1:def 1;
hence x in E by A1; :: thesis: verum