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