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: for a being set st a is_min_depend PA,PB holds

a is_min_depend PB,PA ;

A29: for a being set st a is_min_depend PB,PA holds

a is_min_depend PA,PB ;

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 ) by A28, A29;

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

( 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: for a being set st a is_min_depend PA,PB holds

a is_min_depend PB,PA ;

A29: for a being set st a is_min_depend PB,PA holds

a is_min_depend PA,PB ;

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 ) by A28, A29;

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