reconsider A = the carrier of Y0 as Subset of Y by Lm3;

thus ( not Y0 is T_0 or Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & 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 ) ) :: thesis: ( ( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & 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 ) ) implies Y0 is T_0 )

( 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 ) ) ; :: thesis: Y0 is T_0

thus ( not Y0 is T_0 or Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & 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 ) ) :: thesis: ( ( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & 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 ) ) implies Y0 is T_0 )

proof

assume A14:
( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for V being Subset of Y holds
assume A1:
Y0 is T_0
; :: thesis: ( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & 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 ) )

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

hereby :: thesis: verum

assume A2:
not Y0 is empty
; :: thesis: for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for E being Subset of Y holds

( not E is open or not x in E or y in E ) ) holds

ex F being Subset of Y st

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

let x, y be Point of Y; :: thesis: ( x is Point of Y0 & y is Point of Y0 & x <> y & ( for E being Subset of Y holds

( not E is open or not x in E or y in E ) ) implies ex F being Subset of Y st

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

assume ( x is Point of Y0 & y is Point of Y0 ) ; :: thesis: ( not x <> y or ex E being Subset of Y st

( E is open & x in E & not y in E ) or ex F being Subset of Y st

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

then reconsider x0 = x, y0 = y as Point of Y0 ;

assume A3: x <> y ; :: thesis: ( ex E being Subset of Y st

( E is open & x in E & not y in E ) or ex F being Subset of Y st

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

( E is open & x in E & not y in E ) or ex F being Subset of Y st

( F is open & not x in F & y in F ) ) ; :: thesis: verum

end;( not E is open or not x in E or y in E ) ) holds

ex F being Subset of Y st

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

let x, y be Point of Y; :: thesis: ( x is Point of Y0 & y is Point of Y0 & x <> y & ( for E being Subset of Y holds

( not E is open or not x in E or y in E ) ) implies ex F being Subset of Y st

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

assume ( x is Point of Y0 & y is Point of Y0 ) ; :: thesis: ( not x <> y or ex E being Subset of Y st

( E is open & x in E & not y in E ) or ex F being Subset of Y st

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

then reconsider x0 = x, y0 = y as Point of Y0 ;

assume A3: x <> y ; :: thesis: ( ex E being Subset of Y st

( E is open & x in E & not y in E ) or ex F being Subset of Y st

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

now :: thesis: ( ex E being Subset of Y st

( E is open & x in E & not y in E ) or ex F being Subset of Y st

( F is open & not x in F & y in F ) )end;

hence
( ex E being Subset of Y st ( E is open & x in E & not y in E ) or ex F being Subset of Y st

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

per cases
( ex E0 being Subset of Y0 st

( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st

( F0 is open & not x0 in F0 & y0 in F0 ) ) by A1, A2, A3;

end;

( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st

( F0 is open & not x0 in F0 & y0 in F0 ) ) by A1, A2, A3;

suppose
ex E0 being Subset of Y0 st

( E0 is open & x0 in E0 & not y0 in E0 ) ; :: thesis: ( ex E being Subset of Y st

( E is open & x in E & not y in E ) or ex F being Subset of Y st

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

( E0 is open & x0 in E0 & not y0 in E0 ) ; :: thesis: ( ex E being Subset of Y st

( E is open & x in E & not y in E ) or ex F being Subset of Y st

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

then consider E0 being Subset of Y0 such that

A4: E0 is open and

A5: x0 in E0 and

A6: not y0 in E0 ;

( E is open & x in E & not y in E ) or ex F being Subset of Y st

( F is open & not x in F & y in F ) ) ; :: thesis: verum

end;A4: E0 is open and

A5: x0 in E0 and

A6: not y0 in E0 ;

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

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

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

consider E being Subset of Y such that

A7: E is open and

A8: E0 = E /\ A by A4, Def1;

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

thus E is open by A7; :: thesis: ( x in E & not y in E )

E /\ A c= E by XBOOLE_1:17;

hence x in E by A5, A8; :: thesis: not y in E

thus not y in E by A2, A6, A8, XBOOLE_0:def 4; :: thesis: verum

end;A7: E is open and

A8: E0 = E /\ A by A4, Def1;

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

thus E is open by A7; :: thesis: ( x in E & not y in E )

E /\ A c= E by XBOOLE_1:17;

hence x in E by A5, A8; :: thesis: not y in E

thus not y in E by A2, A6, A8, XBOOLE_0:def 4; :: thesis: verum

( E is open & x in E & not y in E ) or ex F being Subset of Y st

( F is open & not x in F & y in F ) ) ; :: thesis: verum

suppose
ex F0 being Subset of Y0 st

( F0 is open & not x0 in F0 & y0 in F0 ) ; :: thesis: ( ex E being Subset of Y st

( E is open & x in E & not y in E ) or ex F being Subset of Y st

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

( F0 is open & not x0 in F0 & y0 in F0 ) ; :: thesis: ( ex E being Subset of Y st

( E is open & x in E & not y in E ) or ex F being Subset of Y st

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

then consider F0 being Subset of Y0 such that

A9: F0 is open and

A10: not x0 in F0 and

A11: y0 in F0 ;

( E is open & x in E & not y in E ) or ex F being Subset of Y st

( F is open & not x in F & y in F ) ) ; :: thesis: verum

end;A9: F0 is open and

A10: not x0 in F0 and

A11: y0 in F0 ;

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

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

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

consider F being Subset of Y such that

A12: F is open and

A13: F0 = F /\ A by A9, Def1;

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

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

thus not x in F by A2, A10, A13, XBOOLE_0:def 4; :: thesis: y in F

F /\ A c= F by XBOOLE_1:17;

hence y in F by A11, A13; :: thesis: verum

end;A12: F is open and

A13: F0 = F /\ A by A9, Def1;

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

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

thus not x in F by A2, A10, A13, XBOOLE_0:def 4; :: thesis: y in F

F /\ A c= F by XBOOLE_1:17;

hence y in F by A11, A13; :: thesis: verum

( E is open & x in E & not y in E ) or ex F being Subset of Y st

( F is open & not x in F & y in F ) ) ; :: thesis: verum

( E is open & x in E & not y in E ) or ex F being Subset of Y st

( F is open & not x in F & y in F ) ) ; :: 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 ) ) ; :: thesis: Y0 is T_0

now :: thesis: ( not Y0 is empty implies for x0, y0 being Point of Y0 holds

( not x0 <> y0 or ex E0 being Subset of Y0 st

( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st

( F0 is open & not x0 in F0 & y0 in F0 ) ) )

hence
Y0 is T_0
; :: thesis: verum( not x0 <> y0 or ex E0 being Subset of Y0 st

( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st

( F0 is open & not x0 in F0 & y0 in F0 ) ) )

A15:
the carrier of Y0 c= the carrier of Y
by Def1;

assume A16: not Y0 is empty ; :: thesis: for x0, y0 being Point of Y0 holds

( not x0 <> y0 or ex E0 being Subset of Y0 st

( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st

( F0 is open & not x0 in F0 & y0 in F0 ) )

let x0, y0 be Point of Y0; :: thesis: ( not x0 <> y0 or ex E0 being Subset of Y0 st

( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st

( F0 is open & not x0 in F0 & y0 in F0 ) )

the carrier of Y0 <> {} by A16;

then ( x0 in the carrier of Y0 & y0 in the carrier of Y0 ) ;

then reconsider x = x0, y = y0 as Point of Y by A15;

assume A17: x0 <> y0 ; :: thesis: ( ex E0 being Subset of Y0 st

( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st

( F0 is open & not x0 in F0 & y0 in F0 ) )

( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st

( F0 is open & not x0 in F0 & y0 in F0 ) ) ; :: thesis: verum

end;assume A16: not Y0 is empty ; :: thesis: for x0, y0 being Point of Y0 holds

( not x0 <> y0 or ex E0 being Subset of Y0 st

( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st

( F0 is open & not x0 in F0 & y0 in F0 ) )

let x0, y0 be Point of Y0; :: thesis: ( not x0 <> y0 or ex E0 being Subset of Y0 st

( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st

( F0 is open & not x0 in F0 & y0 in F0 ) )

the carrier of Y0 <> {} by A16;

then ( x0 in the carrier of Y0 & y0 in the carrier of Y0 ) ;

then reconsider x = x0, y = y0 as Point of Y by A15;

assume A17: x0 <> y0 ; :: thesis: ( ex E0 being Subset of Y0 st

( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st

( F0 is open & not x0 in F0 & y0 in F0 ) )

now :: thesis: ( ex E0 being Subset of Y0 st

( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st

( F0 is open & not x0 in F0 & y0 in F0 ) )end;

hence
( ex E0 being Subset of Y0 st ( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st

( F0 is open & not x0 in F0 & y0 in F0 ) )

per cases
( ex E being Subset of Y st

( E is open & x in E & not y in E ) or ex F being Subset of Y st

( F is open & not x in F & y in F ) ) by A14, A16, A17;

end;

( E is open & x in E & not y in E ) or ex F being Subset of Y st

( F is open & not x in F & y in F ) ) by A14, A16, A17;

suppose
ex E being Subset of Y st

( E is open & x in E & not y in E ) ; :: thesis: ( ex E0 being Subset of Y0 st

( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st

( F0 is open & not x0 in F0 & y0 in F0 ) )

( E is open & x in E & not y in E ) ; :: thesis: ( ex E0 being Subset of Y0 st

( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st

( F0 is open & not x0 in F0 & y0 in F0 ) )

then consider E being Subset of Y such that

A18: E is open and

A19: x in E and

A20: not y in E ;

( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st

( F0 is open & not x0 in F0 & y0 in F0 ) ) ; :: thesis: verum

end;A18: E is open and

A19: x in E and

A20: not y in E ;

now :: thesis: ex E0 being Subset of Y0 st

( E0 is open & x0 in E0 & not y0 in E0 )

hence
( ex E0 being Subset of Y0 st ( E0 is open & x0 in E0 & not y0 in E0 )

consider E0 being Subset of Y0 such that

A21: E0 is open and

A22: E0 = E /\ A by A18, Th1;

take E0 = E0; :: thesis: ( E0 is open & x0 in E0 & not y0 in E0 )

thus E0 is open by A21; :: thesis: ( x0 in E0 & not y0 in E0 )

thus x0 in E0 by A16, A19, A22, XBOOLE_0:def 4; :: thesis: not y0 in E0

end;A21: E0 is open and

A22: E0 = E /\ A by A18, Th1;

take E0 = E0; :: thesis: ( E0 is open & x0 in E0 & not y0 in E0 )

thus E0 is open by A21; :: thesis: ( x0 in E0 & not y0 in E0 )

thus x0 in E0 by A16, A19, A22, XBOOLE_0:def 4; :: thesis: not y0 in E0

now :: thesis: not y0 in E0

hence
not y0 in E0
; :: thesis: verumA23:
E /\ A c= E
by XBOOLE_1:17;

assume y0 in E0 ; :: thesis: contradiction

hence contradiction by A20, A22, A23; :: thesis: verum

end;assume y0 in E0 ; :: thesis: contradiction

hence contradiction by A20, A22, A23; :: thesis: verum

( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st

( F0 is open & not x0 in F0 & y0 in F0 ) ) ; :: thesis: verum

suppose
ex F being Subset of Y st

( F is open & not x in F & y in F ) ; :: thesis: ( ex E0 being Subset of Y0 st

( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st

( F0 is open & not x0 in F0 & y0 in F0 ) )

( F is open & not x in F & y in F ) ; :: thesis: ( ex E0 being Subset of Y0 st

( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st

( F0 is open & not x0 in F0 & y0 in F0 ) )

then consider F being Subset of Y such that

A24: F is open and

A25: not x in F and

A26: y in F ;

( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st

( F0 is open & not x0 in F0 & y0 in F0 ) ) ; :: thesis: verum

end;A24: F is open and

A25: not x in F and

A26: y in F ;

now :: thesis: ex F0 being Subset of Y0 st

( F0 is open & not x0 in F0 & y0 in F0 )

hence
( ex E0 being Subset of Y0 st ( F0 is open & not x0 in F0 & y0 in F0 )

consider F0 being Subset of Y0 such that

A27: F0 is open and

A28: F0 = F /\ A by A24, Th1;

take F0 = F0; :: thesis: ( F0 is open & not x0 in F0 & y0 in F0 )

thus F0 is open by A27; :: thesis: ( not x0 in F0 & y0 in F0 )

thus y0 in F0 by A16, A26, A28, XBOOLE_0:def 4; :: thesis: verum

end;A27: F0 is open and

A28: F0 = F /\ A by A24, Th1;

take F0 = F0; :: thesis: ( F0 is open & not x0 in F0 & y0 in F0 )

thus F0 is open by A27; :: thesis: ( not x0 in F0 & y0 in F0 )

now :: thesis: not x0 in F0

hence
not x0 in F0
; :: thesis: y0 in F0A29:
F /\ A c= F
by XBOOLE_1:17;

assume x0 in F0 ; :: thesis: contradiction

hence contradiction by A25, A28, A29; :: thesis: verum

end;assume x0 in F0 ; :: thesis: contradiction

hence contradiction by A25, A28, A29; :: thesis: verum

thus y0 in F0 by A16, A26, A28, XBOOLE_0:def 4; :: thesis: verum

( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st

( F0 is open & not x0 in F0 & y0 in F0 ) ) ; :: thesis: verum

( E0 is open & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st

( F0 is open & not x0 in F0 & y0 in F0 ) ) ; :: thesis: verum