let IT, PA, PB be a_partition of Y; :: thesis: ( ( for d being set holds
( d in IT iff d is_min_depend PA,PB ) ) implies for d being set holds
( d in IT iff d is_min_depend PB,PA ) )

A28: now

let a be set ; :: thesis: ( a is_min_depend PA,PB implies a is_min_depend PB,PA )
assume A29: a is_min_depend PA,PB ; :: thesis: a is_min_depend PB,PA
then A30: ( a is_a_dependent_set_of PB & a is_a_dependent_set_of PA ) by Def2;
for d being set st d c= a & d is_a_dependent_set_of PB & d is_a_dependent_set_of PA holds
d = a by A29, Def2;
hence a is_min_depend PB,PA by A30, Def2; :: thesis: verum

end;

A31: now

let a be set ; :: thesis: ( a is_min_depend PB,PA implies a is_min_depend PA,PB )
assume A32: a is_min_depend PB,PA ; :: thesis: a is_min_depend PA,PB
then A33: ( a is_a_dependent_set_of PA & a is_a_dependent_set_of PB ) by Def2;
for d being set st d c= a & d is_a_dependent_set_of PA & d is_a_dependent_set_of PB holds
d = a by A32, Def2;
hence a is_min_depend PA,PB by A33, Def2; :: thesis: verum

end;

for a being set st ( for d being set holds
( d in a iff d is_min_depend PA,PB ) ) holds
for d being set holds
( d in a iff d is_min_depend PB,PA )

proof

let a be set ; :: thesis: ( ( for d being set holds
( d in a iff d is_min_depend PA,PB ) ) implies for d being set holds
( d in a iff d is_min_depend PB,PA ) )
assume A34: for d being set holds
( d in a iff d is_min_depend PA,PB ) ; :: thesis: for d being set holds
( d in a iff d is_min_depend PB,PA )
let d be set ; :: thesis: ( d in a iff d is_min_depend PB,PA )
A35: ( d in a iff d is_min_depend PA,PB ) by A34;
hence ( d in a implies d is_min_depend PB,PA ) by A28; :: thesis: ( d is_min_depend PB,PA implies d in a )
assume d is_min_depend PB,PA ; :: thesis: d in a
hence d in a by A31, A35; :: thesis: verum

end;

hence ( ( for d being set holds
( d in IT iff d is_min_depend PA,PB ) ) implies for d being set holds
( d in IT iff d is_min_depend PB,PA ) ) ; :: thesis: verum