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
A1: not D in {{}} by TARSKI:def 1;
assume D c= X ; :: thesis: D in BOOL X
hence D in BOOL X by A1, XBOOLE_0:def 5; :: thesis: verum
end;
assume D in BOOL X ; :: thesis: D c= X
hence D c= X ; :: thesis: verum