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 that
A1: p <= q and
A2: q <= r ; :: thesis: p <= r
A3: q `2 c= r `2 by A2, Def10;
p `2 c= q `2 by A1, Def10;
then A4: p `2 c= r `2 by A3, XBOOLE_1:1;
A5: r `1 c= q `1 by A2, Def10;
q `1 c= p `1 by A1, Def10;
then r `1 c= p `1 by A5, XBOOLE_1:1;
hence p <= r by A4, Def10; :: thesis: verum