let T be non empty TopPoset; :: thesis:
assume A1: T is lower ; :: thesis:

assume not T is empty ; :: thesis:
let x, y be Point of T; :: thesis:
assume A2: x <> y ; :: thesis:
reconsider a = x, b = y as Element of T ;
set Vy = (uparrow a) ` ;
set Vx = (uparrow b) ` ;
a <= a ;
then A3: not x in (uparrow a) ` by YELLOW_9:1;
b <= b ;
then A4: not y in (uparrow b) ` by YELLOW_9:1;
A5: (uparrow b) ` is open by A1, Th4;
A6: (uparrow a) ` is open by A1, Th4;

per cases by A2, YELLOW_0:def 3;

suppose not b <= a ; :: thesis:

then a in (uparrow b) ` by YELLOW_9:1;
hence ( ex V being Subset of T st
( V is open & x in V & not y in V ) or ex V being Subset of T st
( V is open & not x in V & y in V ) ) by A5, A4; :: thesis:

end;

suppose not a <= b ; :: thesis:

then b in (uparrow a) ` by YELLOW_9:1;
hence ( ex V being Subset of T st
( V is open & x in V & not y in V ) or ex V being Subset of T st
( V is open & not x in V & y in V ) ) by A6, A3; :: thesis:

end;

end;

end;

hence T is T_0 by TSP_1:def 3; :: thesis: