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

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