let Y be non empty TopStruct ; :: thesis: for A, B being Subset of Y st ( A is closed or B is closed ) & A is T_0 & B is T_0 holds
A \/ B is T_0

let A, B be Subset of Y; :: thesis: ( ( A is closed or B is closed ) & A is T_0 & B is T_0 implies A \/ B is T_0 )
assume A1: ( A is closed or B is closed ) ; :: thesis: ( not A is T_0 or not B is T_0 or A \/ B is T_0 )
assume that
A2: A is T_0 and
A3: B is T_0 ; :: thesis: A \/ B is T_0
now :: thesis: for x, y being Point of Y st x in A \/ B & y in A \/ B & x <> y & ( for V being Subset of Y holds
( not V is closed or not x in V or y in V ) ) holds
ex W being Subset of Y st
( W is closed & not x in W & y in W )
let x, y be Point of Y; :: thesis: ( x in A \/ B & y in A \/ B & x <> y & ( for V being Subset of Y holds
( not V is closed or not x in V or y in V ) ) implies ex W being Subset of Y st
( W is closed & not x in W & y in W ) )

assume A4: ( x in A \/ B & y in A \/ B ) ; :: thesis: ( not x <> y or ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) )

then A5: ( x in (A \ B) \/ B & y in (A \ B) \/ B ) by XBOOLE_1:39;
assume A6: x <> y ; :: thesis: ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) )

A7: ( x in A \/ (B \ A) & y in A \/ (B \ A) ) by ;
now :: thesis: ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) )
per cases ( A is closed or B is closed ) by A1;
suppose A8: A is closed ; :: thesis: ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) )

now :: thesis: ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) )
per cases ( ( x in A & y in A ) or ( x in A & y in B \ A ) or ( x in B \ A & y in A ) or ( x in B \ A & y in B \ A ) ) by ;
suppose ( x in A & y in A ) ; :: thesis: ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) )

hence ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) ) by A2, A6; :: thesis: verum
end;
suppose A9: ( x in A & y in B \ A ) ; :: thesis: ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) )

now :: thesis: ex A being Subset of Y st
( A is closed & x in A & not y in A )
take A = A; :: thesis: ( A is closed & x in A & not y in A )
thus A is closed by A8; :: thesis: ( x in A & not y in A )
thus x in A by A9; :: thesis: not y in A
thus not y in A by ; :: thesis: verum
end;
hence ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) ) ; :: thesis: verum
end;
suppose A10: ( x in B \ A & y in A ) ; :: thesis: ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) )

now :: thesis: ex A being Subset of Y st
( A is closed & not x in A & y in A )
take A = A; :: thesis: ( A is closed & not x in A & y in A )
thus A is closed by A8; :: thesis: ( not x in A & y in A )
thus not x in A by ; :: thesis: y in A
thus y in A by A10; :: thesis: verum
end;
hence ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) ) ; :: thesis: verum
end;
suppose A11: ( x in B \ A & y in B \ A ) ; :: thesis: ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) )

B \ A c= B by XBOOLE_1:36;
hence ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) ) by A3, A6, A11; :: thesis: verum
end;
end;
end;
hence ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) ) ; :: thesis: verum
end;
suppose A12: B is closed ; :: thesis: ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) )

now :: thesis: ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) )
per cases ( ( x in A \ B & y in A \ B ) or ( x in A \ B & y in B ) or ( x in B & y in A \ B ) or ( x in B & y in B ) ) by ;
suppose A13: ( x in A \ B & y in A \ B ) ; :: thesis: ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) )

A \ B c= A by XBOOLE_1:36;
hence ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) ) by A2, A6, A13; :: thesis: verum
end;
suppose A14: ( x in A \ B & y in B ) ; :: thesis: ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) )

now :: thesis: ex B being Subset of Y st
( B is closed & not x in B & y in B )
take B = B; :: thesis: ( B is closed & not x in B & y in B )
thus B is closed by A12; :: thesis: ( not x in B & y in B )
thus not x in B by ; :: thesis: y in B
thus y in B by A14; :: thesis: verum
end;
hence ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) ) ; :: thesis: verum
end;
suppose A15: ( x in B & y in A \ B ) ; :: thesis: ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) )

now :: thesis: ex B being Subset of Y st
( B is closed & x in B & not y in B )
take B = B; :: thesis: ( B is closed & x in B & not y in B )
thus B is closed by A12; :: thesis: ( x in B & not y in B )
thus x in B by A15; :: thesis: not y in B
thus not y in B by ; :: thesis: verum
end;
hence ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) ) ; :: thesis: verum
end;
suppose ( x in B & y in B ) ; :: thesis: ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) )

hence ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) ) by A3, A6; :: thesis: verum
end;
end;
end;
hence ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) ) ; :: thesis: verum
end;
end;
end;
hence ( ex V being Subset of Y st
( V is closed & x in V & not y in V ) or ex W being Subset of Y st
( W is closed & not x in W & y in W ) ) ; :: thesis: verum
end;
hence A \/ B is T_0 ; :: thesis: verum