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 )
A1: the InternalRel of N is_reflexive_in the carrier of N by ORDERS_2:def 4;
A2: the InternalRel of N is_transitive_in the carrier of N by ORDERS_2:def 5;
the InternalRel of N is_antisymmetric_in the carrier of N by ORDERS_2:def 6;
hence ( N is reflexive & N is transitive & N is antisymmetric ) by A1, A2, ORDERS_2:def 4, ORDERS_2:def 5, ORDERS_2:def 6; :: thesis: N is directed
A3: 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 A3, Th3; :: according to WAYBEL_0:def 6 :: thesis: verum