let A1 be SetSequence of {1,2,3,4}; for w being Real st ( w = 1 or w = 3 ) & ( for n being Nat holds
( A1 . n = {} or A1 . n = {1,2} or A1 . n = {3,4} or A1 . n = {1,2,3,4} ) ) holds
{w} <> Intersection A1
let w be Real; ( ( w = 1 or w = 3 ) & ( for n being Nat holds
( A1 . n = {} or A1 . n = {1,2} or A1 . n = {3,4} or A1 . n = {1,2,3,4} ) ) implies {w} <> Intersection A1 )
assume KX:
( w = 1 or w = 3 )
; ( ex n being Nat st
( not A1 . n = {} & not A1 . n = {1,2} & not A1 . n = {3,4} & not A1 . n = {1,2,3,4} ) or {w} <> Intersection A1 )
assume S2:
for n being Nat holds
( A1 . n = {} or A1 . n = {1,2} or A1 . n = {3,4} or A1 . n = {1,2,3,4} )
; {w} <> Intersection A1