let x, y, z be object ; :: thesis: ( x in field (R \~) & y in field (R \~) & z in field (R \~) & [x,y] in R \~ & [y,z] in R \~ implies [x,z] in R \~ )
assume that
x in field (R \~) and
y in field (R \~) and
z in field (R \~) and
A2: [x,y] in R \~ and
A3: [y,z] in R \~ ; :: thesis: [x,z] in R \~
A4: x in field R by A2, RELAT_1:15;
A5: y in field R by A2, RELAT_1:15;
A6: z in field R by A3, RELAT_1:15;
then A7: [x,z] in R by A1, A2, A3, A4, A5;
not [x,y] in R ~ by A2, XBOOLE_0:def 5;
then not [y,x] in R by RELAT_1:def 7;
then not [z,x] in R by A1, A3, A4, A5, A6;
then not [x,z] in R ~ by RELAT_1:def 7;
hence [x,z] in R \~ by A7, XBOOLE_0:def 5; :: thesis: verum