let T be set ; :: thesis: {} is empty Subset-Family of
consider F being empty Subset-Family of ;
F = {} ;
hence {} is empty Subset-Family of ; :: thesis: verum