set y = {1,2,3};
not 4 in {1,2,3} by ENUMSET1:def 1;
then b1: {1,2,3} <> {1,2,3,4} by ENUMSET1:def 2;
3 in {1,2,3} by ENUMSET1:def 1;
then K1: {1,2,3} <> {1,2} by TARSKI:def 2;
( not {1,2,3} in {{},{1,2}} & not {1,2,3} in {{3,4}} )

proof

( not {1,2,3} in {{}} & not {1,2,3} in {{1,2}} ) by K1, TARSKI:def 1;
then not {1,2,3} in {{}} \/ {{1,2}} by XBOOLE_0:def 3;
hence ( not {1,2,3} in {{},{1,2}} & not {1,2,3} in {{3,4}} ) by TARSKI:def 1, WW1, ENUMSET1:1; :: thesis: verum

end;

then not {1,2,3} in {{},{1,2}} \/ {{3,4}} by XBOOLE_0:def 3;
then ( not {1,2,3} in {{},{1,2},{3,4}} & not {1,2,3} in {{1,2,3,4}} ) by b1, ENUMSET1:3, TARSKI:def 1;
then not {1,2,3} in {{},{1,2},{3,4}} \/ {{1,2,3,4}} by XBOOLE_0:def 3;
hence {{},{1,2},{3,4},{1,2,3,4}} <> bool {1,2,3,4} by B123, ENUMSET1:6; :: thesis: verum