theorem Th36: :: EUCLID12:48

for A, B, C being Point of (TOP-REAL 2)
for L1, L2 being Element of line_of_REAL 2
for D being Point of (TOP-REAL 2) st L1 _|_ L2 & L1 = Line (A,B) & L2 = Line (C,D) holds
|((B - A),(D - C))| = 0