let X be set ; :: thesis: for S being Subset-Family of X st FinMeetCl S is with_non-empty_elements holds
S is with_non-empty_elements
let S be Subset-Family of X; :: thesis: ( FinMeetCl S is with_non-empty_elements implies S is with_non-empty_elements )
assume A1: FinMeetCl S is with_non-empty_elements ; :: thesis: S is with_non-empty_elements
assume not S is with_non-empty_elements ; :: thesis: contradiction
then ( {} in S & S c= FinMeetCl S ) by CANTOR_1:4;
hence contradiction by A1; :: thesis: verum