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;

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 = {}

hence
( PA \ B c= PA & PA \ B <> {} & X ` = union (PA \ B) )
by A6, EQREL_1:43, XBOOLE_1:36; :: thesis: verumassume
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;then PA c= B by XBOOLE_1:37;

hence contradiction by A2, A4, A5, XBOOLE_0:def 10; :: thesis: verum