let Y be non empty set ; :: thesis: for PA being a_partition of Y
for X being Subset of Y st X is_a_dependent_set_of PA & X <> Y holds
X ` is_a_dependent_set_of PA
let PA be a_partition of Y; :: thesis: for X being Subset of Y st X is_a_dependent_set_of PA & X <> Y holds
X ` is_a_dependent_set_of PA
let X be Subset of Y; :: thesis: ( X is_a_dependent_set_of PA & X <> Y implies X ` is_a_dependent_set_of PA )
assume A1: ( X is_a_dependent_set_of PA & X <> Y ) ; :: thesis: X ` is_a_dependent_set_of PA
then consider B being set such that
A2: ( B c= PA & B <> {} & X = union B ) by Def1;
take PA \ B ; :: according to PARTIT1:def 1 :: thesis: ( PA \ B c= PA & PA \ B <> {} & X ` = union (PA \ B) )
A3: ( union PA = Y & ( for A being set st A in PA holds
( A <> {} & ( for B being set holds
( not B in PA or A = B or A misses B ) ) ) ) ) by EQREL_1:def 6;
then A4: X ` = (union PA) \ (union B) by A2, SUBSET_1:def 5;
reconsider B = B as Subset of PA by A2;

now

assume PA \ B = {} ; :: thesis: contradiction
then PA c= B by XBOOLE_1:37;
hence contradiction by A1, A2, A3, XBOOLE_0:def 10; :: thesis: verum

end;

hence ( PA \ B c= PA & PA \ B <> {} & X ` = union (PA \ B) ) by A4, EQREL_1:52, XBOOLE_1:36; :: thesis: verum