let x, y, z be Element of (FinSups f); :: according to YELLOW_0:def 2 :: thesis: ( not x <= y or not y <= z or x <= z )
assume A1: ( x <= y & y <= z ) ; :: thesis: x <= z
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 WAYBEL_2:def 2;
A3: InclPoset (Fin J) = RelStr(# (Fin J),(RelIncl (Fin J)) #) by YELLOW_1:def 1;
then reconsider x1 = x, y1 = y, z1 = z as Element of (InclPoset (Fin J)) by A2;
( x1 <= y1 & y1 <= z1 ) by A1, A2, A3, YELLOW_0:1;
then ( x1 c= y1 & y1 c= z1 ) by YELLOW_1:3;
then x1 c= z1 by XBOOLE_1:1;
then x1 <= z1 by YELLOW_1:3;
hence x <= z by A2, A3, YELLOW_0:1; :: thesis: verum