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 ( p <= q & q <= p ) ; :: thesis: p = q
then ( p `1 c= q `1 & q `2 c= p `2 & q `1 c= p `1 & p `2 c= q `2 ) by Def10;
then A1: ( p `1 = q `1 & p `2 = q `2 ) by XBOOLE_0:def 10;
( p = [(p `1 ),(p `2 )] & q = [(q `1 ),(q `2 )] ) by MCART_1:24;
hence p = q by A1; :: thesis: verum