let X be non empty set ; :: thesis: for Y being empty Subset-Family of X holds Y is in_general_position
let Y be empty Subset-Family of X; :: thesis: Y is in_general_position
not {} in {X} by TARSKI:def 1;
then not {} in Components Y by Th13;
hence Y is in_general_position ; :: thesis: verum