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 ) )

A61: now

let a be set ; :: thesis: ( a is_min_depend PA,PB implies a is_min_depend PB,PA )
assume A62: a is_min_depend PA,PB ; :: thesis: a is_min_depend PB,PA
A63: ( a is_a_dependent_set_of PB & a is_a_dependent_set_of PA ) by A62, Def2;
A64: 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 A62, Def2;
thus a is_min_depend PB,PA by A63, A64, Def2; :: thesis: verum

end;

A65: now

let a be set ; :: thesis: ( a is_min_depend PB,PA implies a is_min_depend PA,PB )
assume A66: a is_min_depend PB,PA ; :: thesis: a is_min_depend PA,PB
A67: ( a is_a_dependent_set_of PA & a is_a_dependent_set_of PB ) by A66, Def2;
A68: 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 A66, Def2;
thus a is_min_depend PA,PB by A67, A68, Def2; :: thesis: verum

end;

A69: 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 A70: 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 )
A71: ( d in a iff d is_min_depend PA,PB ) by A70;
thus ( d in a implies d is_min_depend PB,PA ) by A61, A71; :: thesis: ( d is_min_depend PB,PA implies d in a )
assume A72: d is_min_depend PB,PA ; :: thesis: d in a
thus d in a by A65, A71, A72; :: thesis: verum

end;

thus ( ( 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 ) ) by A69; :: thesis: verum