let L be non empty 1-sorted ; :: thesis: for N being net of
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 ; :: 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 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 )
then reconsider N' = N " A as strict subnet of N by YELLOW_6:31;
take N' ; :: thesis: ( rng the mapping of N' c= A & N' is SubNetStr of N )
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
A1: x in dom the mapping of N' and
A2: y = the mapping of N' . x by FUNCT_1:def 5;
A3: x in dom (the mapping of N | the carrier of N') by A1, YELLOW_6:def 8;
then x in (dom the mapping of N) /\ the carrier of N' by RELAT_1:90;
then x in the carrier of N' by XBOOLE_0:def 4;
then A4: x in the mapping of N " A by YELLOW_6:def 13;
y = (the mapping of N | the carrier of N') . x by A2, YELLOW_6:def 8;
then y = the mapping of N . x by A3, FUNCT_1:70;
hence y in A by A4, FUNCT_1:def 13; :: thesis: verum

end;

hence ( rng the mapping of N' c= A & N' is SubNetStr of N ) ; :: thesis: verum