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

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

hence
( rng the mapping of N9 c= A & N9 is SubNetStr of N )
; :: thesis: verum
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;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