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