let S be non empty 1-sorted ; :: thesis: for N being net of S
for M being subnet of N
for X being set st M is_often_in X holds
N is_often_in X
let N be net of S; :: thesis: for M being subnet of N
for X being set st M is_often_in X holds
N is_often_in X
let M be subnet of N; :: thesis: for X being set st M is_often_in X holds
N is_often_in X
let X be set ; :: thesis: ( M is_often_in X implies N is_often_in X )
assume A1: M is_often_in X ; :: thesis: N is_often_in X
let i be Element of N; :: according to WAYBEL_0:def 12 :: thesis: ex b₁ being Element of the carrier of N st
( i <= b₁ & N . b₁ in X )
consider f being Function of M,N such that
A2: the mapping of M = the mapping of N * f and
A3: 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 by Def9;
consider n being Element of M such that
A4: for p being Element of M st n <= p holds
i <= f . p by A3;
consider m being Element of M such that
A5: n <= m and
A6: M . m in X by A1;
take f . m ; :: thesis: ( i <= f . m & N . (f . m) in X )
thus i <= f . m by A4, A5; :: thesis: N . (f . m) in X
thus N . (f . m) in X by A2, A6, FUNCT_2:15; :: thesis: verum