:: deftheorem defines _|_ EUCLIDLP:def 8 :
for n being Nat
for L1, L2 being Element of line_of_REAL n holds
( L1 _|_ L2 iff ex x1, x2, y1, y2 being Element of REAL n st
( L1 = Line (x1,x2) & L2 = Line (y1,y2) & x2 - x1 _|_ y2 - y1 ) );