let X be non empty set ; :: thesis: for Y being finite Subset-Family of X st Y is in_general_position holds

Components Y is a_partition of X

let Y be finite Subset-Family of X; :: thesis: ( Y is in_general_position implies Components Y is a_partition of X )

assume Y is in_general_position ; :: thesis: Components Y is a_partition of X

then A1: for A being Subset of X st A in Components Y holds

( A <> {} & ( for B being Subset of X holds

( not B in Components Y or A = B or A misses B ) ) ) by Th16;

union (Components Y) = X by Th15;

hence Components Y is a_partition of X by A1, EQREL_1:def 4; :: thesis: verum

Components Y is a_partition of X

let Y be finite Subset-Family of X; :: thesis: ( Y is in_general_position implies Components Y is a_partition of X )

assume Y is in_general_position ; :: thesis: Components Y is a_partition of X

then A1: for A being Subset of X st A in Components Y holds

( A <> {} & ( for B being Subset of X holds

( not B in Components Y or A = B or A misses B ) ) ) by Th16;

union (Components Y) = X by Th15;

hence Components Y is a_partition of X by A1, EQREL_1:def 4; :: thesis: verum