let Y be non empty TopStruct ; :: thesis: for F being Subset-Family of Y st F is anti-discrete-set-family holds
meet F is anti-discrete
let F be Subset-Family of Y; :: thesis: ( F is anti-discrete-set-family implies meet F is anti-discrete )
assume A1: F is anti-discrete-set-family ; :: thesis: meet F is anti-discrete

hereby :: thesis: verum

per cases ( meet F = {} or meet F <> {} ) ;

suppose meet F = {} ; :: thesis: meet F is anti-discrete

hence meet F is anti-discrete ; :: thesis: verum

end;

suppose meet F <> {} ; :: thesis: meet F is anti-discrete

meet F c= union F by SETFAM_1:2;
hence meet F is anti-discrete by A1, Th5, Th8; :: thesis: verum

end;

end;

end;