consider X being with_suprema Poset;
consider M being Function of the carrier of X,the carrier of L;
take N = NetStr(# the carrier of X,the InternalRel of X,M #); :: thesis: ( not N is empty & N is reflexive & N is transitive & N is antisymmetric & N is directed )
thus not N is empty ; :: thesis: ( N is reflexive & N is transitive & N is antisymmetric & N is directed )
( the InternalRel of N is_reflexive_in the carrier of N & the InternalRel of N is_transitive_in the carrier of N & the InternalRel of N is_antisymmetric_in the carrier of N ) by ORDERS_2:def 4, ORDERS_2:def 5, ORDERS_2:def 6;
hence ( N is reflexive & N is transitive & N is antisymmetric ) by ORDERS_2:def 4, ORDERS_2:def 5, ORDERS_2:def 6; :: thesis: N is directed
A1: RelStr(# the carrier of N,the InternalRel of N #) = RelStr(# the carrier of X,the InternalRel of X #) ;
[#] X = [#] N ;
hence [#] N is directed by A1, Th3; :: according to WAYBEL_0:def 6 :: thesis: verum