thus {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{},{2,3}} c= {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}} \/ {{2,3}} :: according to XBOOLE_0:def 10 :: thesis: {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}} \/ {{2,3}} c= {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{},{2,3}}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{},{2,3}} or x in {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}} \/ {{2,3}} )
assume x in {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{},{2,3}} ; :: thesis: x in {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}} \/ {{2,3}}
then ( x = {1,2,3,4} or x = {1,2,3} or x = {2,3,4} or x = {1} or x = {2} or x = {3} or x = {4} or x = {} or x = {2,3} ) by ENUMSET1:def 7;
then ( x in {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}} or x in {{2,3}} ) by ENUMSET1:def 6, TARSKI:def 1;
hence x in {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}} \/ {{2,3}} by XBOOLE_0:def 3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}} \/ {{2,3}} or x in {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{},{2,3}} )
assume x in {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}} \/ {{2,3}} ; :: thesis: x in {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{},{2,3}}
then ( x in {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{}} or x in {{2,3}} ) by XBOOLE_0:def 3;
then ( x = {1,2,3,4} or x = {1,2,3} or x = {2,3,4} or x = {1} or x = {2} or x = {3} or x = {4} or x = {} or x = {2,3} ) by ENUMSET1:def 6, TARSKI:def 1;
hence x in {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{},{2,3}} by ENUMSET1:def 7; :: thesis: verum