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:19;

now

let x, y, z be set ; :: 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 x' = x, y' = y, z' = z as Element of L by A1, A2, A3, A4;
reconsider x' = x', y' = y', z' = z' as Element of L ;
A7: x' <= y' by A5, Def4;
z' <= z' ;
hence [x,z] in AR by A6, A7, Def5; :: 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