let L be non empty 1-sorted ; :: thesis: for N being net of L
for A being set st N is_often_in A holds
ex N' being strict subnet of N st
( rng the mapping of N' c= A & N' is SubNetStr of N )
let N be net of L; :: thesis: for A being set st N is_often_in A holds
ex N' being strict subnet of N st
( rng the mapping of N' c= A & N' is SubNetStr of N )
let A be set ; :: thesis: ( N is_often_in A implies ex N' being strict subnet of N st
( rng the mapping of N' c= A & N' is SubNetStr of N ) )
assume A1: N is_often_in A ; :: thesis: ex N' being strict subnet of N st
( rng the mapping of N' c= A & N' is SubNetStr of N )
reconsider N' = N " A as strict subnet of N by A1, YELLOW_6:31;
A2: rng the mapping of N' c= A

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng the mapping of N' or y in A )
assume y in rng the mapping of N' ; :: thesis: y in A
then consider x being set such that
A3: ( x in dom the mapping of N' & y = the mapping of N' . x ) by FUNCT_1:def 5;
A4: x in dom (the mapping of N | the carrier of N') by A3, YELLOW_6:def 8;
then x in (dom the mapping of N) /\ the carrier of N' by RELAT_1:90;
then A5: ( x in dom the mapping of N & x in the carrier of N' ) by XBOOLE_0:def 4;
y = (the mapping of N | the carrier of N') . x by A3, YELLOW_6:def 8;
then A6: y = the mapping of N . x by A4, FUNCT_1:70;
x in the mapping of N " A by A5, YELLOW_6:def 13;
hence y in A by A6, FUNCT_1:def 13; :: thesis: verum

end;

take N' ; :: thesis: ( rng the mapping of N' c= A & N' is SubNetStr of N )
thus ( rng the mapping of N' c= A & N' is SubNetStr of N ) by A2; :: thesis: verum