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;
A3: ex_sup_of f .: x,L by YELLOW_0:17;
A4: ex_sup_of f .: y,L by YELLOW_0:17;
( g . x = sup (f .: x) & g . y = sup (f .: y) ) by A2;
then reconsider fx = g . x as Element of L ;
A5: 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;
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 A6: ( a = (netmap (FinSups f),L) . x & b = (netmap (FinSups f),L) . y ) ; :: thesis: a <= b
x1 <= y1 by A1, A2, A5, YELLOW_0:1;
then x c= y by YELLOW_1:3;
then sup (f .: x) <= sup (f .: y) by A3, A4, RELAT_1:156, YELLOW_0:34;
then fx <= sup (f .: y) by A2;
hence a <= b by A2, A6; :: thesis: verum