let T be 1-sorted ; :: thesis: for P being Subset of T holds
( P <> [#] T iff ([#] T) \ P <> {} )
let P be Subset of T; :: thesis: ( P <> [#] T iff ([#] T) \ P <> {} )

now

assume A1: ( P <> [#] T & ([#] T) \ P = {} ) ; :: thesis: contradiction
then ( [#] T c= P & P c= [#] T ) by XBOOLE_1:37;
hence contradiction by A1, XBOOLE_0:def 10; :: thesis: verum

end;

hence ( P <> [#] T iff ([#] T) \ P <> {} ) by XBOOLE_1:37; :: thesis: verum