suppose A1: Y <> {} ; :: thesis:

set H9 = {Y};
reconsider H = {Y} as Subset-Family of Y by ZFMISC_1:68;
H is hierarchic

let x, y be set ; :: according to TAXONOM2:def 3 :: thesis:
assume that
A2: x in H and
A3: y in H ; :: thesis:
x = Y by A2, TARSKI:def 1;
hence ( x c= y or y c= x or x misses y ) by A3; :: thesis:

end;

then reconsider H = H as Hierarchy of Y by Def4;
take H ; :: thesis:
union H = Y by ZFMISC_1:25;
hence H is covering by ABIAN:4; :: thesis:
thus H is T_3 :: thesis:

let A be Subset of Y; :: according to TAXONOM2:def 6 :: thesis:
assume A in H ; :: thesis:
then A4: A = Y by TARSKI:def 1;
let x be Element of Y; :: thesis:
assume not x in A ; :: thesis:
hence ex B being Subset of Y st
( x in B & B in H & A misses B ) by A1, A4; :: thesis:

end;

end;

suppose A5: Y = {} ; :: thesis:

set H9 = {} ;
reconsider H = {} as Subset-Family of Y by XBOOLE_1:2;
reconsider H1 = H as Hierarchy of Y by Def4, Th5;
take H1 ; :: thesis:
thus H1 is covering by A5, ABIAN:4, ZFMISC_1:2; :: thesis:
thus H1 is T_3 ; :: thesis:

end;

end;