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

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

end;