theorem Th48: :: JGRAPH_6:48

for a, b, c, d being Real
for f1, f2 being FinSequence of (TOP-REAL 2)
for p0, p1, p01, p10 being Point of (TOP-REAL 2) st a < b & c < d & p0 = |[a,c]| & p1 = |[b,d]| & p01 = |[a,d]| & p10 = |[b,c]| & f1 = <*p0,p01,p1*> & f2 = <*p0,p10,p1*> holds
( f1 is being_S-Seq & L~ f1 = (LSeg (p0,p01)) \/ (LSeg (p01,p1)) & f2 is being_S-Seq & L~ f2 = (LSeg (p0,p10)) \/ (LSeg (p10,p1)) & rectangle (a,b,c,d) = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {p0,p1} & f1 /. 1 = p0 & f1 /. (len f1) = p1 & f2 /. 1 = p0 & f2 /. (len f2) = p1 )