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;
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; verum