let E be set ; :: thesis: for A being Subset of E holds
( A c= A ` iff A = {} E )
let A be Subset of E; :: thesis: ( A c= A ` iff A = {} E )
thus ( A c= A ` implies A = {} E ) by XBOOLE_1:38; :: thesis: ( A = {} E implies A c= A ` )
A in bool E by Def2;
hence ( A = {} E implies A c= A ` ) by ZFMISC_1:def 1; :: thesis: verum