reconsider A = the carrier of Y0 as Subset of Y byLm3; thus
( not Y0 is V144() 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 E being Subset of Y holds ( not E is closed or not x in E or y in E ) ) holds ex F being Subset of Y st ( F is closed & not x in F & y in F ) )
:: 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 E being Subset of Y holds ( not E is closed or not x in E or y in E ) ) holds ex F being Subset of Y st ( F is closed & not x in F & y in F ) ) implies Y0 is T_0 )
assume A1:
Y0 is V144()
; :: 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 E being Subset of Y holds ( not E is closed or not x in E or y in E ) ) holds ex F being Subset of Y st ( F is closed & not x in F & y in F ) )
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 closed or not x in E or y in E ) ) holds ex F being Subset of Y st ( F is closed & 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 closed or not x in E or y in E ) ) implies ex F being Subset of Y st ( F is closed & 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 closed & x in E & not y in E ) or ex F being Subset of Y st ( F is closed & 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 closed & x in E & not y in E ) or ex F being Subset of Y st ( F is closed & not x in F & y in F ) )
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 E being Subset of Y holds ( not E is closed or not x in E or y in E ) ) holds ex F being Subset of Y st ( F is closed & not x in F & y in F ) )
; :: 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 closed & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st ( F0 is closed & not x0 in F0 & y0 in F0 ) ) )
hence
( ex E0 being Subset of Y0 st ( E0 is closed & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st ( F0 is closed & not x0 in F0 & y0 in F0 ) )
; :: thesis: verum
hence
( ex E0 being Subset of Y0 st ( E0 is closed & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st ( F0 is closed & not x0 in F0 & y0 in F0 ) )
; :: thesis: verum
end;
end;
end;
hence
( ex E0 being Subset of Y0 st ( E0 is closed & x0 in E0 & not y0 in E0 ) or ex F0 being Subset of Y0 st ( F0 is closed & not x0 in F0 & y0 in F0 ) )
; :: thesis: verum