let T be non empty TopSpace; :: thesis: for s being sequence of the carrier of T
for x being Point of T
for B being basis of (BOOL2F (NeighborhoodSystem x)) holds
( ( for b being Element of B ex i being Element of OrderedNAT st
for j being Element of OrderedNAT st i <= j holds
s . j in b ) iff for b being Element of B ex i being Element of (sequence_to_net s) st
for j being Element of (sequence_to_net s) st i <= j holds
(sequence_to_net s) . j in b )
let s be sequence of the carrier of T; :: thesis: for x being Point of T
for B being basis of (BOOL2F (NeighborhoodSystem x)) holds
( ( for b being Element of B ex i being Element of OrderedNAT st
for j being Element of OrderedNAT st i <= j holds
s . j in b ) iff for b being Element of B ex i being Element of (sequence_to_net s) st
for j being Element of (sequence_to_net s) st i <= j holds
(sequence_to_net s) . j in b )
let x be Point of T; :: thesis: for B being basis of (BOOL2F (NeighborhoodSystem x)) holds
( ( for b being Element of B ex i being Element of OrderedNAT st
for j being Element of OrderedNAT st i <= j holds
s . j in b ) iff for b being Element of B ex i being Element of (sequence_to_net s) st
for j being Element of (sequence_to_net s) st i <= j holds
(sequence_to_net s) . j in b )
let B be basis of (BOOL2F (NeighborhoodSystem x)); :: thesis: ( ( for b being Element of B ex i being Element of OrderedNAT st
for j being Element of OrderedNAT st i <= j holds
s . j in b ) iff for b being Element of B ex i being Element of (sequence_to_net s) st
for j being Element of (sequence_to_net s) st i <= j holds
(sequence_to_net s) . j in b )
A1: ( ( for b being Element of B ex i being Element of OrderedNAT st
for j being Element of OrderedNAT st i <= j holds
s . j in b ) implies for b being Element of B ex i being Element of (sequence_to_net s) st
for j being Element of (sequence_to_net s) st i <= j holds
(sequence_to_net s) . j in b )

proof

assume A2: for b being Element of B ex i being Element of OrderedNAT st
for j being Element of OrderedNAT st i <= j holds
s . j in b ; :: thesis: for b being Element of B ex i being Element of (sequence_to_net s) st
for j being Element of (sequence_to_net s) st i <= j holds
(sequence_to_net s) . j in b
for b being Element of B ex i being Element of (sequence_to_net s) st
for j being Element of (sequence_to_net s) st i <= j holds
(sequence_to_net s) . j in b

proof

let b be Element of B; :: thesis: ex i being Element of (sequence_to_net s) st
for j being Element of (sequence_to_net s) st i <= j holds
(sequence_to_net s) . j in b
consider i being Element of OrderedNAT such that
A3: for j being Element of OrderedNAT st i <= j holds
s . j in b by A2;
reconsider i0 = i as Element of (sequence_to_net s) ;
for j being Element of (sequence_to_net s) st i0 <= j holds
(sequence_to_net s) . j in b

proof

let j be Element of (sequence_to_net s); :: thesis: ( i0 <= j implies (sequence_to_net s) . j in b )
assume A4: i0 <= j ; :: thesis: (sequence_to_net s) . j in b
reconsider j0 = j as Element of OrderedNAT ;
( the mapping of (sequence_to_net s) . j = s . j0 & i <= j0 ) by A4;
hence (sequence_to_net s) . j in b by A3; :: thesis: verum

end;

hence ex i being Element of (sequence_to_net s) st
for j being Element of (sequence_to_net s) st i <= j holds
(sequence_to_net s) . j in b ; :: thesis: verum

end;

hence for b being Element of B ex i being Element of (sequence_to_net s) st
for j being Element of (sequence_to_net s) st i <= j holds
(sequence_to_net s) . j in b ; :: thesis: verum

end;

( ( for b being Element of B ex i being Element of (sequence_to_net s) st
for j being Element of (sequence_to_net s) st i <= j holds
(sequence_to_net s) . j in b ) implies for b being Element of B ex i being Element of OrderedNAT st
for j being Element of OrderedNAT st i <= j holds
s . j in b )

proof

assume A5: for b being Element of B ex i being Element of (sequence_to_net s) st
for j being Element of (sequence_to_net s) st i <= j holds
(sequence_to_net s) . j in b ; :: thesis: for b being Element of B ex i being Element of OrderedNAT st
for j being Element of OrderedNAT st i <= j holds
s . j in b
for b being Element of B ex i being Element of OrderedNAT st
for j being Element of OrderedNAT st i <= j holds
s . j in b

proof

let b be Element of B; :: thesis: ex i being Element of OrderedNAT st
for j being Element of OrderedNAT st i <= j holds
s . j in b
consider i being Element of (sequence_to_net s) such that
A6: for j being Element of (sequence_to_net s) st i <= j holds
(sequence_to_net s) . j in b by A5;
reconsider i0 = i as Element of OrderedNAT ;
for j being Element of OrderedNAT st i0 <= j holds
s . j in b

proof

let j be Element of OrderedNAT; :: thesis: ( i0 <= j implies s . j in b )
assume A7: i0 <= j ; :: thesis: s . j in b
reconsider j0 = j as Element of (sequence_to_net s) ;
( the mapping of (sequence_to_net s) . j0 = s . j & i <= j0 ) by A7;
then ( (sequence_to_net s) . j0 in b & i <= j0 ) by A6;
hence s . j in b ; :: thesis: verum

end;

hence ex i being Element of OrderedNAT st
for j being Element of OrderedNAT st i <= j holds
s . j in b ; :: thesis: verum

end;

hence for b being Element of B ex i being Element of OrderedNAT st
for j being Element of OrderedNAT st i <= j holds
s . j in b ; :: thesis: verum

end;

hence ( ( for b being Element of B ex i being Element of OrderedNAT st
for j being Element of OrderedNAT st i <= j holds
s . j in b ) iff for b being Element of B ex i being Element of (sequence_to_net s) st
for j being Element of (sequence_to_net s) st i <= j holds
(sequence_to_net s) . j in b ) by A1; :: thesis: verum