let E be set ; :: thesis: for A being Subset of E st ( for x being Element of E holds x in A ) holds
E = A
let A be Subset of E; :: thesis: ( ( for x being Element of E holds x in A ) implies E = A )
assume A1: for x being Element of E holds x in A ; :: thesis: E = A
thus E c= A :: according to XBOOLE_0:def 10 :: thesis: A c= E

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in E or a in A )
assume A2: a in E ; :: thesis: a in A
reconsider a = a as set by TARSKI:1;
a is Element of E by Def1, A2;
hence a in A by A1; :: thesis: verum

end;

A in bool E by Def1;
hence A c= E by ZFMISC_1:def 1; :: thesis: verum