let x, E be set ; :: thesis: for A being Subset of E st x in A holds
x is Element of E
let A be Subset of E; :: thesis: ( x in A implies x is Element of E )
assume x in A ; :: thesis: x is Element of E
then x in E by Lm1;
hence x is Element of E by Def2; :: thesis: verum