let S be non empty 1-sorted ; :: thesis:
let N be net of S; :: thesis:
let X be set ; :: thesis:
assume A1: N is_often_in X ; :: thesis:
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:
reconsider M = N " X as non empty full SubNetStr of N by A3, Def10;
M is directed

let i, j be Element of M; :: according to YELLOW_6:def 3 :: thesis:
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:
( x <= e & y <= e ) by A4, A5, YELLOW_0:def 2;
hence ( i <= k & j <= k ) by Th12; :: thesis:

end;