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 that
A1: x <= y and
A2: y <= z ; :: thesis: x <= z
A3: ( ex g being Function of (Fin J), the carrier of L st
for x being Element of Fin J holds
( g . x = sup (f .: x) & FinSups f = NetStr(# (Fin J),(RelIncl (Fin J)),g #) ) & InclPoset (Fin J) = RelStr(# (Fin J),(RelIncl (Fin J)) #) ) by WAYBEL_2:def 2, YELLOW_1:def 1;
then reconsider x1 = x, y1 = y, z1 = z as Element of (InclPoset (Fin J)) ;
y1 <= z1 by A2, A3;
then A4: y1 c= z1 by YELLOW_1:3;
x1 <= y1 by A1, A3;
then x1 c= y1 by YELLOW_1:3;
then x1 c= z1 by A4;
then x1 <= z1 by YELLOW_1:3;
hence x <= z by A3; :: thesis: verum