theorem Th63: :: JGRAPH_6:63

for x being set
for a, b, c, d being Real st x in rectangle (a,b,c,d) & a < b & c < d & not x in LSeg (|[a,c]|,|[a,d]|) & not x in LSeg (|[a,d]|,|[b,d]|) & not x in LSeg (|[b,d]|,|[b,c]|) holds
x in LSeg (|[b,c]|,|[a,c]|)