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

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