let e be set ; :: thesis: for n being Element of NAT st e in Seg n holds
ex i being Element of NAT st
( e = i & 1 <= i & i <= n )
let n be Element of NAT ; :: thesis: ( e in Seg n implies ex i being Element of NAT st
( e = i & 1 <= i & i <= n ) )
assume A1: e in Seg n ; :: thesis: ex i being Element of NAT st
( e = i & 1 <= i & i <= n )
then reconsider e = e as Element of NAT ;
take e ; :: thesis: ( e = e & 1 <= e & e <= n )
thus ( e = e & 1 <= e & e <= n ) by A1, FINSEQ_1:1; :: thesis: verum