set X = the with_suprema Poset;
set M = the Function of the carrier of the with_suprema Poset, the carrier of L;
take N = NetStr(# the carrier of the with_suprema Poset, the InternalRel of the with_suprema Poset, the Function of the carrier of the with_suprema Poset, the carrier of L #); :: 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 2;
A2: the InternalRel of N is_transitive_in the carrier of N by ORDERS_2:def 3;
the InternalRel of N is_antisymmetric_in the carrier of N by ORDERS_2:def 4;
hence ( N is reflexive & N is transitive & N is antisymmetric ) by A1, A2, ORDERS_2:def 2, ORDERS_2:def 3, ORDERS_2:def 4; :: thesis: N is directed
A3: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of the with_suprema Poset, the InternalRel of the with_suprema Poset #) ;
[#] the with_suprema Poset = [#] N ;
hence [#] N is directed by A3, Th3; :: according to WAYBEL_0:def 6 :: thesis: verum