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₁, b₂ being Element of the carrier of L holds
( not b₁ = (netmap ((FinSups f),L)) . x or not b₂ = (netmap ((FinSups f),L)) . y or b₁ <= b₂ ) )
assume A1: x <= y ; :: thesis: for b₁, b₂ being Element of the carrier of L holds
( not b₁ = (netmap ((FinSups f),L)) . x or not b₂ = (netmap ((FinSups f),L)) . y or b₁ <= 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