let Y be non empty TopStruct ; :: thesis:
let A, B be Subset of Y; :: thesis:
assume A1: ( A is open or B is open ) ; :: thesis:
assume that
A2: A is T_0 and
A3: B is T_0 ; :: thesis:

now :: thesis:

let x, y be Point of Y; :: thesis:
assume A4: ( x in A \/ B & y in A \/ B ) ; :: thesis:
then A5: ( x in (A \ B) \/ B & y in (A \ B) \/ B ) by XBOOLE_1:39;
assume A6: x <> y ; :: thesis:
A7: ( x in A \/ (B \ A) & y in A \/ (B \ A) ) by A4, XBOOLE_1:39;

now :: thesis:

per cases by A1;

suppose A8: A is open ; :: thesis:

now :: thesis:

per cases by A7, XBOOLE_0:def 3;

suppose ( x in A & y in A ) ; :: thesis:

hence ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) by A2, A6; :: thesis:

end;

suppose A9: ( x in A & y in B \ A ) ; :: thesis:

now :: thesis:

take A = A; :: thesis:
thus A is open by A8; :: thesis:
thus x in A by A9; :: thesis:
thus not y in A by A9, XBOOLE_0:def 5; :: thesis:

end;

hence ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) ; :: thesis:

end;

suppose A10: ( x in B \ A & y in A ) ; :: thesis:

now :: thesis:

take A = A; :: thesis:
thus A is open by A8; :: thesis:
thus not x in A by A10, XBOOLE_0:def 5; :: thesis:
thus y in A by A10; :: thesis:

end;

hence ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) ; :: thesis:

end;

suppose A11: ( x in B \ A & y in B \ A ) ; :: thesis:

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

end;

end;

end;

hence ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) ; :: thesis:

end;

suppose A12: B is open ; :: thesis:

now :: thesis:

per cases by A5, XBOOLE_0:def 3;

suppose A13: ( x in A \ B & y in A \ B ) ; :: thesis:

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

end;

suppose A14: ( x in A \ B & y in B ) ; :: thesis:

now :: thesis:

take B = B; :: thesis:
thus B is open by A12; :: thesis:
thus not x in B by A14, XBOOLE_0:def 5; :: thesis:
thus y in B by A14; :: thesis:

end;

hence ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) ; :: thesis:

end;

suppose A15: ( x in B & y in A \ B ) ; :: thesis:

now :: thesis:

take B = B; :: thesis:
thus B is open by A12; :: thesis:
thus x in B by A15; :: thesis:
thus not y in B by A15, XBOOLE_0:def 5; :: thesis:

end;

hence ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) ; :: thesis:

end;

suppose ( x in B & y in B ) ; :: thesis:

hence ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) by A3, A6; :: thesis:

end;

end;

end;

hence ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) ; :: thesis:

end;

end;

end;

hence ( ex V being Subset of Y st
( V is open & x in V & not y in V ) or ex W being Subset of Y st
( W is open & not x in W & y in W ) ) ; :: thesis:

end;

hence A \/ B is T_0 ; :: thesis: