let X be set ; :: thesis: for D being non empty set holds
( D c= X iff D in BOOL X )
let D be non empty set ; :: thesis: ( D c= X iff D in BOOL X )
thus ( D c= X implies D in BOOL X ) :: thesis: ( D in BOOL X implies D c= X )

proof

assume D c= X ; :: thesis: D in BOOL X
then ( D in bool X & not D in {{} } ) by TARSKI:def 1;
hence D in BOOL X by XBOOLE_0:def 5; :: thesis: verum

end;

assume D in BOOL X ; :: thesis: D c= X
hence D c= X ; :: thesis: verum