theorem :: CARDFIL4:63

for x being object
for i, j being Nat
for T being non empty TopSpace
for s being Function of [:NAT,NAT:], the carrier of T holds
( x in s .: ([:NAT,NAT:] \ [:(Segm i),(Segm j):]) iff ex n, m being Nat st
( ( i <= n or j <= m ) & x = s . (n,m) ) )