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 A2: ( A is T_0 & B is T_0 ) ; :: thesis: A \/ B is T_0
now
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 A3: ( 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 A4: ( x in A \/ (B \ A) & y in A \/ (B \ A) ) by XBOOLE_1:39;
A5: ( x in (A \ B) \/ B & y in (A \ B) \/ B ) by A3, 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 ) )
now
per cases ( A is closed or B is closed ) by A1;
suppose A7: 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
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 A4, XBOOLE_0:def 3;
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, Def9; :: thesis: verum
end;
suppose A8: ( 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
take A = A; :: thesis: ( A is closed & x in A & not y in A )
thus A is closed by A7; :: thesis: ( x in A & not y in A )
thus x in A by A8; :: thesis: not y in A
thus not y in A by A8, XBOOLE_0:def 5; :: 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 A9: ( 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
take A = A; :: thesis: ( A is closed & not x in A & y in A )
thus A is closed by A7; :: thesis: ( not x in A & y in A )
thus not x in A by A9, XBOOLE_0:def 5; :: thesis: y in A
thus y in A by A9; :: 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 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 A2, A6, A10, Def9; :: 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 A11: 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
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;
suppose A12: ( 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, A12, Def9; :: thesis: verum
end;
suppose A13: ( 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
take B = B; :: thesis: ( B is closed & not x in B & y in B )
thus B is closed by A11; :: thesis: ( not x in B & y in B )
thus not x in B by A13, XBOOLE_0:def 5; :: thesis: y in B
thus y in B by A13; :: 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 A14: ( 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
take B = B; :: thesis: ( B is closed & x in B & not y in B )
thus B is closed by A11; :: thesis: ( x in B & not y in B )
thus x in B by A14; :: thesis: not y in B
thus not y in B by A14, XBOOLE_0:def 5; :: 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 A2, A6, Def9; :: 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 by Def9; :: thesis: verum