let S be non empty 1-sorted ; :: thesis: for N being net of S
for X being set st N is_often_in X holds
N " X is subnet of N
let N be net of S; :: thesis: for X being set st N is_often_in X holds
N " X is subnet of N
let X be set ; :: thesis: ( N is_often_in X implies N " X is subnet of N )
assume A1: N is_often_in X ; :: thesis: N " X is subnet of N
then reconsider M = N " X as net of S by Th21;
M is subnet of N
proof
set f = id M;
the carrier of M c= the carrier of N by Th10;
then reconsider f = id M as Function of M,N by FUNCT_2:7;
take f ; :: according to YELLOW_6:def 9 :: thesis: ( the mapping of M = the mapping of N * f & ( for m being Element of N ex n being Element of M st
for p being Element of M st n <= p holds
m <= f . p ) )
the mapping of M = the mapping of N | the carrier of M by Def6;
hence the mapping of M = the mapping of N * f by RELAT_1:65; :: thesis: for m being Element of N ex n being Element of M st
for p being Element of M st n <= p holds
m <= f . p
let m be Element of N; :: thesis: ex n being Element of M st
for p being Element of M st n <= p holds
m <= f . p
consider j being Element of N such that
A2: m <= j and
A3: N . j in X by A1;
j in the mapping of N " X by A3, FUNCT_2:38;
then reconsider n = j as Element of M by Def10;
take n ; :: thesis: for p being Element of M st n <= p holds
m <= f . p
let p be Element of M; :: thesis: ( n <= p implies m <= f . p )
assume A4: n <= p ; :: thesis: m <= f . p
j <= f . p by A4, Th11;
hence m <= f . p by A2, YELLOW_0:def 2; :: thesis: verum
end;
hence N " X is subnet of N ; :: thesis: verum