let x, y be Element of (FinSups f); :: according to ORDERS_3:def 5,WAYBEL_0:def 9 :: thesis: ( not x <= y or for b_{1}, b_{2} being Element of the carrier of L holds

( not b_{1} = (netmap ((FinSups f),L)) . x or not b_{2} = (netmap ((FinSups f),L)) . y or b_{1} <= b_{2} ) )

assume A1: x <= y ; :: thesis: for b_{1}, b_{2} being Element of the carrier of L holds

( not b_{1} = (netmap ((FinSups f),L)) . x or not b_{2} = (netmap ((FinSups f),L)) . y or b_{1} <= b_{2} )

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 A1, A2, A3, YELLOW_0:1;

then x c= y by YELLOW_1:3;

then sup (f .: x) <= sup (f .: y) by A4, RELAT_1:123, YELLOW_0:34;

then A5: fx <= sup (f .: y) by A2;

let a, b be Element of L; :: thesis: ( not a = (netmap ((FinSups f),L)) . x or not b = (netmap ((FinSups f),L)) . y or a <= b )

assume ( a = (netmap ((FinSups f),L)) . x & b = (netmap ((FinSups f),L)) . y ) ; :: thesis: a <= b

hence a <= b by A2, A5; :: thesis: verum

( not b

assume A1: x <= y ; :: thesis: for b

( not b

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 A1, A2, A3, YELLOW_0:1;

then x c= y by YELLOW_1:3;

then sup (f .: x) <= sup (f .: y) by A4, RELAT_1:123, YELLOW_0:34;

then A5: fx <= sup (f .: y) by A2;

let a, b be Element of L; :: thesis: ( not a = (netmap ((FinSups f),L)) . x or not b = (netmap ((FinSups f),L)) . y or a <= b )

assume ( a = (netmap ((FinSups f),L)) . x & b = (netmap ((FinSups f),L)) . y ) ; :: thesis: a <= b

hence a <= b by A2, A5; :: thesis: verum