per cases ( Y <> {} or Y = {} ) ;

suppose A1: Y <> {} ; :: thesis: ex b₁ being Hierarchy of Y st
( b₁ is covering & b₁ is T_3 )

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

proof

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

end;

then reconsider H = H as Hierarchy of Y by Def4;
take H ; :: thesis: ( H is covering & H is T_3 )
union H = Y by ZFMISC_1:31;
hence H is covering by ABIAN:4; :: thesis: H is T_3
thus H is T_3 :: thesis: verum

proof

let A be Subset of Y; :: according to TAXONOM2:def 6 :: thesis: ( A in H implies for x being Element of Y st not x in A holds
ex B being Subset of Y st
( x in B & B in H & A misses B ) )
assume A3: A in H ; :: thesis: for x being Element of Y st not x in A holds
ex B being Subset of Y st
( x in B & B in H & A misses B )
A4: A = Y by A3, TARSKI:def 1;
let x be Element of Y; :: thesis: ( not x in A implies ex B being Subset of Y st
( x in B & B in H & A misses B ) )
assume A5: not x in A ; :: thesis: ex B being Subset of Y st
( x in B & B in H & A misses B )
thus ex B being Subset of Y st
( x in B & B in H & A misses B ) by A1, A4, A5; :: thesis: verum

end;

end;

suppose A6: Y = {} ; :: thesis: ex b₁ being Hierarchy of Y st
( b₁ is covering & b₁ is T_3 )

set H' = {} ;
reconsider H = {} as Subset-Family of Y by XBOOLE_1:2;
reconsider H1 = H as Hierarchy of Y by Def4, Th6;
take H1 ; :: thesis: ( H1 is covering & H1 is T_3 )
thus H1 is covering by A6, ABIAN:4, ZFMISC_1:2; :: thesis: H1 is T_3
thus H1 is T_3 by Th11; :: thesis: verum

end;

end;