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

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

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

let s be Function of , the carrier of T; :: thesis: ( x in s .: ( \ [:(Segm i),(Segm j):]) iff ex n, m being Nat st
( ( i <= n or j <= m ) & x = s . (n,m) ) )

hereby :: thesis: ( ex n, m being Nat st
( ( i <= n or j <= m ) & x = s . (n,m) ) implies x in s .: ( \ [:(Segm i),(Segm j):]) )
assume x in s .: ( \ [:(Segm i),(Segm j):]) ; :: thesis: ex n, m being Nat st
( ( i <= n or j <= m ) & x = s . (n,m) )

then consider y being object such that
A1: y in dom s and
A2: y in \ [:(Segm i),(Segm j):] and
A3: x = s . y by FUNCT_1:def 6;
reconsider z = y as Element of by A1;
A4: ( not z `1 in Segm i or not z `2 in Segm j )
proof end;
reconsider n = z `1 , m = z `2 as Nat ;
take n = n; :: thesis: ex m being Nat st
( ( i <= n or j <= m ) & x = s . (n,m) )

take m = m; :: thesis: ( ( i <= n or j <= m ) & x = s . (n,m) )
thus ( i <= n or j <= m ) by ; :: thesis: x = s . (n,m)
z is pair by Th4;
hence x = s . (n,m) by ; :: thesis: verum
end;
assume ex n, m being Nat st
( ( i <= n or j <= m ) & x = s . (n,m) ) ; :: thesis: x in s .: ( \ [:(Segm i),(Segm j):])
then consider n, m being Nat such that
A6: ( i <= n or j <= m ) and
A7: x = s . (n,m) ;
( n in NAT & m in NAT ) by ORDINAL1:def 12;
then A8: [n,m] in by ZFMISC_1:def 2;
not [n,m] in [:(Segm i),(Segm j):]
proof
assume [n,m] in [:(Segm i),(Segm j):] ; :: thesis: contradiction
then ex a, b being object st
( a in Segm i & b in Segm j & [n,m] = [a,b] ) by ZFMISC_1:def 2;
then ( n in Segm i & m in Segm j ) by XTUPLE_0:1;
hence contradiction by A6, NAT_1:44; :: thesis: verum
end;
then A9: [n,m] in \ [:(Segm i),(Segm j):] by ;
A10: x = s . [n,m] by ;
[n,m] in dom s by ;
hence x in s .: ( \ [:(Segm i),(Segm j):]) by ; :: thesis: verum