let L be lower-bounded sup-Semilattice; for AR being auxiliary(i) auxiliary(ii) Relation of L holds AR is transitive
let AR be auxiliary(i) auxiliary(ii) Relation of L; AR is transitive
A1:
field AR c= the carrier of L \/ the carrier of L
by RELSET_1:8;
now 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 ARlet x,
y,
z be
object ;
( 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
;
[x,z] in ARreconsider 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;
verum end;
then
AR is_transitive_in field AR
by RELAT_2:def 8;
hence
AR is transitive
by RELAT_2:def 16; verum