let a, b, c be Element of (OASpace (TOP-REAL 2)); :: thesis: ( Mid a,b,c iff ex u, v being Point of (TOP-REAL 2) st
( u = a & v = c & b in LSeg (u,v) ) )

hereby :: thesis: ( ex u, v being Point of (TOP-REAL 2) st
( u = a & v = c & b in LSeg (u,v) ) implies Mid a,b,c )

assume Mid a,b,c ; :: thesis: ex u, v being Point of (TOP-REAL 2) st
( u = a & v = c & b in LSeg (u,v) )

per cases then ( a = b or b = c or ex u, v being Point of (TOP-REAL 2) st
( u = a & v = c & b in LSeg (u,v) ) ) by THSS;

suppose A1: a = b ; :: thesis: ex u, v being Point of (TOP-REAL 2) st
( u = a & v = c & b in LSeg (u,v) )

reconsider u = a, v = c as Point of (TOP-REAL 2) ;
u in LSeg (u,v) by RLTOPSP1:68;
hence ex u, v being Point of (TOP-REAL 2) st
( u = a & v = c & b in LSeg (u,v) ) by A1; :: thesis: verum

end;

suppose A2: b = c ; :: thesis: ex u, v being Point of (TOP-REAL 2) st
( u = a & v = c & b in LSeg (u,v) )

reconsider u = a, v = c as Point of (TOP-REAL 2) ;
v in LSeg (u,v) by RLTOPSP1:68;
hence ex u, v being Point of (TOP-REAL 2) st
( u = a & v = c & b in LSeg (u,v) ) by A2; :: thesis: verum

end;

suppose ex u, v being Point of (TOP-REAL 2) st
( u = a & v = c & b in LSeg (u,v) ) ; :: thesis: ex u, v being Point of (TOP-REAL 2) st
( u = a & v = c & b in LSeg (u,v) )

hence ex u, v being Point of (TOP-REAL 2) st
( u = a & v = c & b in LSeg (u,v) ) ; :: thesis: verum

end;

end;

end;

assume ex u, v being Point of (TOP-REAL 2) st
( u = a & v = c & b in LSeg (u,v) ) ; :: thesis: Mid a,b,c
hence Mid a,b,c by THSS; :: thesis: verum