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

end;

suppose A1:
Y <> {}
; :: thesis: ex b_{1} being Hierarchy of Y st

( b_{1} is covering & b_{1} is T_3 )

( b

set H9 = {Y};

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

H is hierarchic

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

end;reconsider H = {Y} as Subset-Family of Y by ZFMISC_1:68;

H is hierarchic

proof

then reconsider H = H as Hierarchy of Y by Def4;
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;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

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;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

suppose A5:
Y = {}
; :: thesis: ex b_{1} being Hierarchy of Y st

( b_{1} is covering & b_{1} is T_3 )

( b

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;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