let X be set ; :: thesis: for P, Q being Dependency of X st P <= Q & Q <= P holds
P = Q
let p, q be Dependency of X; :: thesis: ( p <= q & q <= p implies p = q )
assume that
A1: p <= q and
A2: q <= p ; :: thesis: p = q
A3: q `1 c= p `1 by A1, Def10;
A4: p `2 c= q `2 by A1, Def10;
q `2 c= p `2 by A2, Def10;
then A5: p `2 = q `2 by A4, XBOOLE_0:def 10;
p `1 c= q `1 by A2, Def10;
then A6: p `1 = q `1 by A3, XBOOLE_0:def 10;
p = [(p `1),(p `2)] by MCART_1:22;
hence p = q by A6, A5, MCART_1:22; :: thesis: verum