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

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

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

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

hereby :: thesis: ( ex i, j being Nat st
( n <= i & n <= j & x = s . (i,j) ) implies x in s .: () )
assume x in s .: () ; :: thesis: ex i, j being Nat st
( n <= i & n <= j & x = s . (i,j) )

then consider y being object such that
A1: y in dom s and
A2: y in square-uparrow n and
A3: x = s . y by FUNCT_1:def 6;
reconsider z = y as Element of by A1;
consider i, j being Nat such that
A4: z `1 = i and
A5: z `2 = j and
A6: n <= i and
A7: n <= j by ;
consider m1, m2 being object such that
m1 in NAT and
m2 in NAT and
A8: z = [m1,m2] by ZFMISC_1:def 2;
x = s . (i,j) by ;
hence ex i, j being Nat st
( n <= i & n <= j & x = s . (i,j) ) by A6, A7; :: thesis: verum
end;
assume ex i, j being Nat st
( n <= i & n <= j & x = s . (i,j) ) ; :: thesis: x in s .: ()
then consider i, j being Nat such that
A9: n <= i and
A10: n <= j and
A11: x = s . (i,j) ;
A12: dom s = by FUNCT_2:def 1;
A13: ( i in NAT & j in NAT ) by ORDINAL1:def 12;
A14: x = s . [i,j] by ;
( [i,j] `1 = i & [i,j] `2 = j & [i,j] in ) by ;
then [i,j] in square-uparrow n by ;
hence x in s .: () by ; :: thesis: verum