let S be non empty 1-sorted ; :: thesis: for N being net of S
for X being set
for M being subnet of N st M = N " X holds
for i being Element of M holds M . i in X
let N be net of S; :: thesis: for X being set
for M being subnet of N st M = N " X holds
for i being Element of M holds M . i in X
let X be set ; :: thesis: for M being subnet of N st M = N " X holds
for i being Element of M holds M . i in X
let M be subnet of N; :: thesis: ( M = N " X implies for i being Element of M holds M . i in X )
assume A1: M = N " X ; :: thesis: for i being Element of M holds M . i in X
let j be Element of M; :: thesis: M . j in X
j in the carrier of M ;
then j in the mapping of N " X by A1, YELLOW_6:def 10;
then A2: the mapping of N . j in X by FUNCT_1:def 7;
the mapping of M = the mapping of N | the carrier of M by A1, YELLOW_6:def 6;
hence M . j in X by A2, FUNCT_1:49; :: thesis: verum