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}}
XBOOLE_0:def 10 {{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 ;
TARSKI:def 3 ( 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}}
;
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;
verum
end;
let x be object ; TARSKI:def 3 ( 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}}
; 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; verum