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