let P, Q be set ; :: thesis: ( P c= Q & P <> Q implies Q \ P <> {} )
assume P c= Q ; :: thesis: ( not P <> Q or Q \ P <> {} )
then A1: Q = P \/ (Q \ P) by XBOOLE_1:45;
assume A2: P <> Q ; :: thesis: Q \ P <> {}
assume Q \ P = {} ; :: thesis: contradiction
hence contradiction by A1, A2; :: thesis: verum