{{},{1,2,3,4}} c= {{},{1,2,3,4}} \/ {{1,2}} by XBOOLE_0:def 3;
then {{},{1,2,3,4}} c= {{},{1,2,3,4},{1,2}} by ENUMSET1:3;
then {{},{1,2,3,4}} c= {{},{1,2,3,4},{1,2}} \/ {{3,4}} by XBOOLE_0:def 3;
then Zw1: {{},{1,2,3,4}} c= {{},{1,2,3,4},{1,2},{3,4}} by ENUMSET1:6;
T1: {{},{1,2,3,4}} c= {{},{1,2},{3,4},{1,2,3,4}}
proof
for x being object st x in {{},{1,2,3,4}} holds
x in {{},{1,2},{3,4},{1,2,3,4}}
proof
let x be object ; :: thesis: ( x in {{},{1,2,3,4}} implies x in {{},{1,2},{3,4},{1,2,3,4}} )
assume ASS1: x in {{},{1,2,3,4}} ; :: thesis: x in {{},{1,2},{3,4},{1,2,3,4}}
( x = {} or x = {1,2,3,4} or x = {1,2} or x = {3,4} ) by ASS1, Zw1, ENUMSET1:def 2;
hence x in {{},{1,2},{3,4},{1,2,3,4}} by ENUMSET1:def 2; :: thesis: verum
end;
hence {{},{1,2,3,4}} c= {{},{1,2},{3,4},{1,2,3,4}} ; :: thesis: verum
end;
set y = {1,2};
C1: {1,2} in {{},{1,2},{3,4},{1,2,3,4}} by ENUMSET1:def 2;
{1,2} <> {1,2,3,4}
proof
( 3 in {1,2,3,4} & not 3 in {1,2} ) by ENUMSET1:def 2, TARSKI:def 2;
hence {1,2} <> {1,2,3,4} ; :: thesis: verum
end;
hence {{},{1,2,3,4}} c< {{},{1,2},{3,4},{1,2,3,4}} by T1, C1, TARSKI:def 2; :: thesis: verum