let x, y be Element of (); :: according to ORDERS_3:def 5,WAYBEL_0:def 9 :: thesis: ( not x <= y or for b1, b2 being Element of the carrier of L holds
( not b1 = (netmap ((),L)) . x or not b2 = (netmap ((),L)) . y or b1 <= b2 ) )

assume A1: x <= y ; :: thesis: for b1, b2 being Element of the carrier of L holds
( not b1 = (netmap ((),L)) . x or not b2 = (netmap ((),L)) . y or b1 <= b2 )

consider g being Function of (Fin J), the carrier of L such that
A2: for x being Element of Fin J holds
( g . x = sup (f .: x) & FinSups f = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) by Def2;
g . x = sup (f .: x) by A2;
then reconsider fx = g . x as Element of L ;
A3: InclPoset (Fin J) = RelStr(# (Fin J),(RelIncl (Fin J)) #) by YELLOW_1:def 1;
then reconsider x1 = x, y1 = y as Element of (InclPoset (Fin J)) by A2;
A4: ( ex_sup_of f .: x,L & ex_sup_of f .: y,L ) by YELLOW_0:17;
x1 <= y1 by ;
then x c= y by YELLOW_1:3;
then sup (f .: x) <= sup (f .: y) by ;
then A5: fx <= sup (f .: y) by A2;
let a, b be Element of L; :: thesis: ( not a = (netmap ((),L)) . x or not b = (netmap ((),L)) . y or a <= b )
assume ( a = (netmap ((),L)) . x & b = (netmap ((),L)) . y ) ; :: thesis: a <= b
hence a <= b by A2, A5; :: thesis: verum