let R be Relation; ( R is transitive iff for x, y, z being object st [x,y] in R & [y,z] in R holds
[x,z] in R )
hereby ( ( for x, y, z being object st [x,y] in R & [y,z] in R holds
[x,z] in R ) implies R is transitive )
assume A1:
R is
transitive
;
for x, y, z being object st [x,y] in R & [y,z] in R holds
[x,z] in Rlet x,
y,
z be
object ;
( [x,y] in R & [y,z] in R implies [x,z] in R )assume that A2:
[x,y] in R
and A3:
[y,z] in R
;
[x,z] in RA4:
z in field R
by A3, RELAT_1:15;
(
x in field R &
y in field R )
by A2, RELAT_1:15;
hence
[x,z] in R
by A1, A2, A3, A4, Def8;
verum
end;
assume
for x, y, z being object st [x,y] in R & [y,z] in R holds
[x,z] in R
; R is transitive
then
for x, y, z being object st x in field R & y in field R & z in field R & [x,y] in R & [y,z] in R holds
[x,z] in R
;
hence
R is_transitive_in field R
; RELAT_2:def 16 verum