thus DIFFERENCE (sring4_8,sring4_8) c= sring4_8 \/ {{1,3,4},{1,2,4},{2,3},{1,3},{1,2},{3,4},{2,4}} :: according to XBOOLE_0:def 10 :: thesis: sring4_8 \/ {{1,3,4},{1,2,4},{2,3},{1,3},{1,2},{3,4},{2,4}} c= DIFFERENCE (sring4_8,sring4_8)
proof
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in DIFFERENCE (sring4_8,sring4_8) or s in sring4_8 \/ {{1,3,4},{1,2,4},{2,3},{1,3},{1,2},{3,4},{2,4}} )
assume s in DIFFERENCE (sring4_8,sring4_8) ; :: thesis: s in sring4_8 \/ {{1,3,4},{1,2,4},{2,3},{1,3},{1,2},{3,4},{2,4}}
then consider x, y being set such that
A1: ( x in sring4_8 & y in sring4_8 ) and
A2: s = x \ y by SETFAM_1:def 6;
( ( 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 = {} ) & ( y = {1,2,3,4} or y = {1,2,3} or y = {2,3,4} or y = {1} or y = {2} or y = {3} or y = {4} or y = {} ) ) by A1, ENUMSET1:def 6;
then ( s = {1,2,3,4} or s = {1,2,3} or s = {2,3,4} or s = {1} or s = {2} or s = {3} or s = {4} or s = {} or s = {1,3,4} or s = {1,2,4} or s = {2,3} or s = {1,3} or s = {1,2} or s = {3,4} or s = {2,4} or s = {2,3} or s = {} ) by GG2, GG3, GG4, GG5, GG6, GG7, XBOOLE_1:37, GG11, GG12, GG13, GG14, GG15, GG18, GG20, GG21, GG22, GG23, GG27, ZFMISC_1:14, GG33, GG34, GG35, GG41, GG42, GG43, GG50, A2;
then ( s in sring4_8 or s in {{1,3,4},{1,2,4},{2,3},{1,3},{1,2},{3,4},{2,4}} ) by ENUMSET1:def 6, ENUMSET1:def 5;
hence s in sring4_8 \/ {{1,3,4},{1,2,4},{2,3},{1,3},{1,2},{3,4},{2,4}} by XBOOLE_0:def 3; :: thesis: verum
end;
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in sring4_8 \/ {{1,3,4},{1,2,4},{2,3},{1,3},{1,2},{3,4},{2,4}} or s in DIFFERENCE (sring4_8,sring4_8) )
assume s in sring4_8 \/ {{1,3,4},{1,2,4},{2,3},{1,3},{1,2},{3,4},{2,4}} ; :: thesis: s in DIFFERENCE (sring4_8,sring4_8)
then ( s in sring4_8 or s in {{1,3,4},{1,2,4},{2,3},{1,3},{1,2},{3,4},{2,4}} ) by XBOOLE_0:def 3;
then VU: ( s = {1,2,3,4} \ {} or s = {1,2,3} \ {} or s = {2,3,4} \ {} or s = {1} \ {} or s = {2} \ {} or s = {3} \ {} or s = {4} \ {} or s = {} \ {} or s = {1} \ {1} or s = {1,2,3,4} \ {2} or s = {1,2,3,4} \ {3} or s = {1,2,3} \ {1} or s = {1,2,3} \ {2} or s = {1,2,3} \ {3} or s = {2,3,4} \ {2} or s = {1,2,3} \ {2,3,4} or s = {2,3,4} \ {3} or s = {1,2,3} \ {1} ) by GG5, GG6, GG12, GG13, GG14, GG21, GG22, ENUMSET1:def 6, ENUMSET1:def 5;
( {1,2,3,4} in sring4_8 & {1,2,3} in sring4_8 & {2,3,4} in sring4_8 & {1} in sring4_8 & {2} in sring4_8 & {3} in sring4_8 & {4} in sring4_8 & {} in sring4_8 ) by ENUMSET1:def 6;
hence s in DIFFERENCE (sring4_8,sring4_8) by VU, SETFAM_1:def 6; :: thesis: verum