let L be lower-bounded sup-Semilattice; :: thesis: for AR being auxiliary(i) auxiliary(ii) Relation of L holds AR is transitive
let AR be auxiliary(i) auxiliary(ii) Relation of L; :: thesis: AR is transitive
A1: field AR c= the carrier of L \/ the carrier of L by RELSET_1:8;

now :: thesis: for x, y, z being object st x in field AR & y in field AR & z in field AR & [x,y] in AR & [y,z] in AR holds
[x,z] in AR

let x, y, z be object ; :: thesis: ( x in field AR & y in field AR & z in field AR & [x,y] in AR & [y,z] in AR implies [x,z] in AR )
assume that
A2: x in field AR and
A3: y in field AR and
A4: z in field AR and
A5: [x,y] in AR and
A6: [y,z] in AR ; :: thesis: [x,z] in AR
reconsider x9 = x, y9 = y, z9 = z as Element of L by A1, A2, A3, A4;
reconsider x9 = x9, y9 = y9, z9 = z9 as Element of L ;
A7: x9 <= y9 by A5, Def3;
z9 <= z9 ;
hence [x,z] in AR by A6, A7, Def4; :: thesis: verum

end;

then AR is_transitive_in field AR by RELAT_2:def 8;
hence AR is transitive by RELAT_2:def 16; :: thesis: verum