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 N9 being strict subnet of N st
( rng the mapping of N9 c= A & N9 is SubNetStr of N )
let N be net of L; :: thesis: for A being set st N is_often_in A holds
ex N9 being strict subnet of N st
( rng the mapping of N9 c= A & N9 is SubNetStr of N )
let A be set ; :: thesis: ( N is_often_in A implies ex N9 being strict subnet of N st
( rng the mapping of N9 c= A & N9 is SubNetStr of N ) )
assume N is_often_in A ; :: thesis: ex N9 being strict subnet of N st
( rng the mapping of N9 c= A & N9 is SubNetStr of N )
then reconsider N9 = N " A as strict subnet of N by YELLOW_6:22;
take N9 ; :: thesis: ( rng the mapping of N9 c= A & N9 is SubNetStr of N )
rng the mapping of N9 c= A
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng the mapping of N9 or y in A )
assume y in rng the mapping of N9 ; :: thesis: y in A
then consider x being object such that
A1: x in dom the mapping of N9 and
A2: y = the mapping of N9 . x by FUNCT_1:def 3;
A3: x in dom ( the mapping of N | the carrier of N9) by A1, YELLOW_6:def 6;
then x in (dom the mapping of N) /\ the carrier of N9 by RELAT_1:61;
then x in the carrier of N9 by XBOOLE_0:def 4;
then A4: x in the mapping of N " A by YELLOW_6:def 10;
y = ( the mapping of N | the carrier of N9) . x by A2, YELLOW_6:def 6;
then y = the mapping of N . x by A3, FUNCT_1:47;
hence y in A by A4, FUNCT_1:def 7; :: thesis: verum
end;
hence ( rng the mapping of N9 c= A & N9 is SubNetStr of N ) ; :: thesis: verum