set H = {} ;
reconsider H9 = {} as Subset-Family of Y by XBOOLE_1:2;
take H9 ; :: thesis: H9 is hierarchic
thus H9 is hierarchic ; :: thesis: verum