let S be non empty 1-sorted ; :: thesis: for N being net of S
for X being set st N is_often_in X holds
( not N " X is empty & N " X is directed )
let N be net of S; :: thesis: for X being set st N is_often_in X holds
( not N " X is empty & N " X is directed )
let X be set ; :: thesis: ( N is_often_in X implies ( not N " X is empty & N " X is directed ) )
assume A1: N is_often_in X ; :: thesis: ( not N " X is empty & N " X is directed )
set i = the Element of N;
consider j being Element of N such that
the Element of N <= j and
A2: N . j in X by A1;
A3: j in the mapping of N " X by A2, FUNCT_2:38;
hence not the carrier of (N " X) is empty by Def10; :: according to STRUCT_0:def 1 :: thesis: N " X is directed
reconsider M = N " X as non empty full SubNetStr of N by A3, Def10;
M is directed

proof

let i, j be Element of M; :: according to YELLOW_6:def 3 :: thesis: ex z being Element of M st
( i <= z & j <= z )
the carrier of M c= the carrier of N by Th10;
then reconsider x = i, y = j as Element of N ;
consider z being Element of N such that
A4: ( x <= z & y <= z ) by Def3;
consider e being Element of N such that
A5: z <= e and
A6: N . e in X by A1;
e in the mapping of N " X by A6, FUNCT_2:38;
then reconsider k = e as Element of M by Def10;
take k ; :: thesis: ( i <= k & j <= k )
( x <= e & y <= e ) by A4, A5, YELLOW_0:def 2;
hence ( i <= k & j <= k ) by Th12; :: thesis: verum

end;

hence N " X is directed ; :: thesis: verum