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 :: thesis: ( P <> [#] T implies not ([#] T) \ P = {} )
assume that
A1: P <> [#] T and
A2: ([#] T) \ P = {} ; :: thesis: contradiction
[#] T c= P by A2, 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