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 A2: ( x in field AR & y in field AR & z in field AR & [x,y] in AR & [y,z] in AR ) ; :: thesis: [x,z] in AR
then reconsider x' = x, y' = y, z' = z as Element of L by A1;
reconsider x' = x', y' = y', z' = z' as Element of L ;
A3: x' <= y' by A2, Def4;
z' <= z' ;
hence [x,z] in AR by A2, A3, 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