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