let X be set ; :: thesis: for P, Q, S being Dependency of X st P <= Q & Q <= S holds
P <= S
let p, q, r be Dependency of X; :: thesis: ( p <= q & q <= r implies p <= r )
assume ( p <= q & q <= r ) ; :: thesis: p <= r
then ( q `1 c= p `1 & p `2 c= q `2 & r `1 c= q `1 & q `2 c= r `2 ) by Def10;
then ( r `1 c= p `1 & p `2 c= r `2 ) by XBOOLE_1:1;
hence p <= r by Def10; :: thesis: verum