let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in INTERSECTION (sring4_8,sring4_8) or s in {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{},{2,3}} )
assume s in INTERSECTION (sring4_8,sring4_8) ; :: thesis: s in {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{},{2,3}}
then consider x, y being set such that
H2: x in sring4_8 and
H3: y in sring4_8 and
H4: s = x /\ y by SETFAM_1:def 5;
( ( 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 H2, H3, ENUMSET1:def 6;
hence s in {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{},{2,3}} by LL2, LL3, LL4, LL5, LL6, LL7, LL10, LL11, LL12, LL13, LL14, LL17, LL18, LL19, LL21, LL22, LL24, LL11a, LL12a, LL13a, LL14a, H4, ENUMSET1:def 7; :: thesis: verum

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 INTERSECTION (sring4_8,sring4_8) )
assume B0: x in {{1,2,3,4},{1,2,3},{2,3,4},{1},{2},{3},{4},{},{2,3}} ; :: thesis: x in INTERSECTION (sring4_8,sring4_8)
( {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;
then ( {1,2,3,4} /\ {1,2,3,4} in INTERSECTION (sring4_8,sring4_8) & {1,2,3} /\ {1,2,3} in INTERSECTION (sring4_8,sring4_8) & {2,3,4} /\ {2,3,4} in INTERSECTION (sring4_8,sring4_8) & {1} /\ {1} in INTERSECTION (sring4_8,sring4_8) & {2} /\ {2} in INTERSECTION (sring4_8,sring4_8) & {3} /\ {3} in INTERSECTION (sring4_8,sring4_8) & {4} /\ {4} in INTERSECTION (sring4_8,sring4_8) & {} /\ {} in INTERSECTION (sring4_8,sring4_8) & {1,2,3} /\ {2,3,4} in INTERSECTION (sring4_8,sring4_8) ) by SETFAM_1:def 5;
hence x in INTERSECTION (sring4_8,sring4_8) by LL10, B0, ENUMSET1:def 7; :: thesis: verum