let R be non empty associative multLoopStr ; :: thesis: for a, b, c being Element of R st a divides b & b divides c holds
a divides c
let A, B, C be Element of R; :: thesis: ( A divides B & B divides C implies A divides C )
now :: thesis: ( A divides B & B divides C & A divides B & B divides C implies A divides C )
assume that
A1: A divides B and
A2: B divides C ; :: thesis: ( A divides B & B divides C implies A divides C )
consider D being Element of R such that
A3: A * D = B by A1;
consider E being Element of R such that
A4: B * E = C by A2;
A * (D * E) = C by A3, A4, GROUP_1:def 3;
hence ( A divides B & B divides C implies A divides C ) ; :: thesis: verum
end;
hence ( A divides B & B divides C implies A divides C ) ; :: thesis: verum