let E be set ; :: thesis: for A being Subset of E
for x being object st x in A holds
x is Element of E
let A be Subset of E; :: thesis: for x being object st x in A holds
x is Element of E
let x be object ; :: thesis: ( x in A implies x is Element of E )
assume A1: x in A ; :: thesis: x is Element of E
reconsider x = x as set by TARSKI:1;
x in E by Lm1, A1;
hence x is Element of E by Def1; :: thesis: verum