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 that
A1: X is_a_dependent_set_of PA and
A2: X <> Y ; :: thesis: X ` is_a_dependent_set_of PA
consider B being set such that
A3: B c= PA and
B <> {} and
A4: X = union B by A1;
take PA \ B ; :: according to PARTIT1:def 1 :: thesis: ( PA \ B c= PA & PA \ B <> {} & X ` = union (PA \ B) )
A5: union PA = Y by EQREL_1:def 4;
then A6: X ` = (union PA) \ (union B) by A4, SUBSET_1:def 4;
reconsider B = B as Subset of PA by A3;

now :: thesis: not PA \ B = {}

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

end;

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