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

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

set H9 = {Y};
reconsider H = {Y} as Subset-Family of Y by ZFMISC_1:68;
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 that
A2: x in H and
A3: y in H ; :: thesis: ( x c= y or y c= x or x misses y )
x = Y by A2, TARSKI:def 1;
hence ( x c= y or y c= x or x misses y ) by A3; :: 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:25;
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 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 )
then A4: A = Y by 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 not x in A ; :: thesis: ex B being Subset of Y st
( x in B & B in H & A misses B )
hence ex B being Subset of Y st
( x in B & B in H & A misses B ) by A1, A4; :: thesis: verum

end;

end;

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

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: ( H1 is covering & H1 is T_3 )
thus H1 is covering by A5, ABIAN:4, ZFMISC_1:2; :: thesis: H1 is T_3
thus H1 is T_3 ; :: thesis: verum

end;

end;