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

A \/ B is T_0

let A, B be Subset of Y; :: thesis: ( ( A is open or B is open ) & A is T_0 & B is T_0 implies A \/ B is T_0 )

assume A1: ( A is open or B is open ) ; :: 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

A \/ B is T_0

let A, B be Subset of Y; :: thesis: ( ( A is open or B is open ) & A is T_0 & B is T_0 implies A \/ B is T_0 )

assume A1: ( A is open or B is open ) ; :: 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 open or not x in V or y in V ) ) holds

ex W being Subset of Y st

( W is open & not x in W & y in W )

hence
A \/ B is T_0
; :: thesis: verum( not V is open or not x in V or y in V ) ) holds

ex W being Subset of Y st

( W is open & 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 open or not x in V or y in V ) ) implies ex W being Subset of Y st

( W is open & 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 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 ) )

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

A7: ( x in A \/ (B \ A) & y in A \/ (B \ A) ) by A4, XBOOLE_1:39;

( 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: verum

end;( not V is open or not x in V or y in V ) ) implies ex W being Subset of Y st

( W is open & 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 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 ) )

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

A7: ( x in A \/ (B \ A) & y in A \/ (B \ A) ) by A4, XBOOLE_1:39;

now :: thesis: ( 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 ) )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 ) )

per cases
( A is open or B is open )
by A1;

end;

suppose A8:
A is open
; :: thesis: ( 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 ) )

( 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: verum

end;

( 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 ) )

now :: thesis: ( 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 ) )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 ) )

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 A7, XBOOLE_0:def 3;

end;

suppose
( x in A & y in A )
; :: thesis: ( 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 ) )

( 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 ) )

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: verum

end;( 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: verum

suppose A9:
( x in A & y in B \ A )
; :: thesis: ( 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 ) )

( 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: verum

end;

( 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 ) )

now :: thesis: ex A being Subset of Y st

( A is open & x in A & not y in A )

hence
( ex V being Subset of Y st ( A is open & x in A & not y in A )

take A = A; :: thesis: ( A is open & x in A & not y in A )

thus A is open 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 A9, XBOOLE_0:def 5; :: thesis: verum

end;thus A is open 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 A9, XBOOLE_0:def 5; :: thesis: verum

( 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: verum

suppose A10:
( x in B \ A & y in A )
; :: thesis: ( 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 ) )

( 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: verum

end;

( 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 ) )

now :: thesis: ex A being Subset of Y st

( A is open & not x in A & y in A )

hence
( ex V being Subset of Y st ( A is open & not x in A & y in A )

take A = A; :: thesis: ( A is open & not x in A & y in A )

thus A is open by A8; :: thesis: ( not x in A & y in A )

thus not x in A by A10, XBOOLE_0:def 5; :: thesis: y in A

thus y in A by A10; :: thesis: verum

end;thus A is open by A8; :: thesis: ( not x in A & y in A )

thus not x in A by A10, XBOOLE_0:def 5; :: thesis: y in A

thus y in A by A10; :: thesis: verum

( 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: verum

suppose A11:
( x in B \ A & y in B \ A )
; :: thesis: ( 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 ) )

( 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 ) )

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: verum

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 ) ) by A3, A6, A11; :: thesis: verum

( 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: verum

suppose A12:
B is open
; :: thesis: ( 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 ) )

( 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: verum

end;

( 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 ) )

now :: thesis: ( 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 ) )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 ) )

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 A5, XBOOLE_0:def 3;

end;

suppose A13:
( x in A \ B & y in A \ B )
; :: thesis: ( 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 ) )

( 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 ) )

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: verum

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 ) ) by A2, A6, A13; :: thesis: verum

suppose A14:
( x in A \ B & y in B )
; :: thesis: ( 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 ) )

( 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: verum

end;

( 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 ) )

now :: thesis: ex B being Subset of Y st

( B is open & not x in B & y in B )

hence
( ex V being Subset of Y st ( B is open & not x in B & y in B )

take B = B; :: thesis: ( B is open & not x in B & y in B )

thus B is open by A12; :: thesis: ( not x in B & y in B )

thus not x in B by A14, XBOOLE_0:def 5; :: thesis: y in B

thus y in B by A14; :: thesis: verum

end;thus B is open by A12; :: thesis: ( not x in B & y in B )

thus not x in B by A14, XBOOLE_0:def 5; :: thesis: y in B

thus y in B by A14; :: thesis: verum

( 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: verum

suppose A15:
( x in B & y in A \ B )
; :: thesis: ( 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 ) )

( 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: verum

end;

( 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 ) )

now :: thesis: ex B being Subset of Y st

( B is open & x in B & not y in B )

hence
( ex V being Subset of Y st ( B is open & x in B & not y in B )

take B = B; :: thesis: ( B is open & x in B & not y in B )

thus B is open 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 A15, XBOOLE_0:def 5; :: thesis: verum

end;thus B is open 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 A15, XBOOLE_0:def 5; :: thesis: verum

( 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: verum

suppose
( x in B & y in B )
; :: thesis: ( 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 ) )

( 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 ) )

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: verum

end;( 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: verum

( 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: verum

( 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: verum