let A, B, C be Point of (TOP-REAL 2); :: thesis: 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

let L1, L2 be Element of line_of_REAL 2; :: thesis: 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

let D be Point of (TOP-REAL 2); :: thesis: ( L1 _|_ L2 & L1 = Line (A,B) & L2 = Line (C,D) implies |((B - A),(D - C))| = 0 )

assume that

A1: L1 _|_ L2 and

A2: L1 = Line (A,B) and

A3: L2 = Line (C,D) ; :: thesis: |((B - A),(D - C))| = 0

consider x1, x2, y1, y2 being Element of REAL 2 such that

A4: L1 = Line (x1,x2) and

A5: L2 = Line (y1,y2) and

A6: x2 - x1 _|_ y2 - y1 by A1, EUCLIDLP:def 8;

A7: |((x2 - x1),(y2 - y1))| = 0 by A6, EUCLIDLP:def 3, RVSUM_1:def 17;

A8: ( A in Line (x1,x2) & B in Line (x1,x2) ) by A2, A4, EUCLID_4:41;

then consider lambda being Real such that

A9: A = ((1 - lambda) * x1) + (lambda * x2) ;

consider mu being Real such that

A10: B = ((1 - mu) * x1) + (mu * x2) by A8;

A11: ( C in Line (y1,y2) & D in Line (y1,y2) ) by A3, A5, EUCLID_4:41;

then consider lambda2 being Real such that

A12: C = ((1 - lambda2) * y1) + (lambda2 * y2) ;

consider mu2 being Real such that

A13: D = ((1 - mu2) * y1) + (mu2 * y2) by A11;

A14: B - A = (mu - lambda) * (x2 - x1) by A9, A10, Th1;

reconsider a = mu - lambda, b = mu2 - lambda2 as Real ;

|((B - A),(D - C))| = |((a * (x2 - x1)),(b * (y2 - y1)))| by A14, A12, A13, Th1

.= a * |((x2 - x1),(b * (y2 - y1)))| by EUCLID_4:21

.= a * (b * |((x2 - x1),(y2 - y1))|) by EUCLID_4:22

.= 0 by A7 ;

hence |((B - A),(D - C))| = 0 ; :: thesis: verum

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

let L1, L2 be Element of line_of_REAL 2; :: thesis: 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

let D be Point of (TOP-REAL 2); :: thesis: ( L1 _|_ L2 & L1 = Line (A,B) & L2 = Line (C,D) implies |((B - A),(D - C))| = 0 )

assume that

A1: L1 _|_ L2 and

A2: L1 = Line (A,B) and

A3: L2 = Line (C,D) ; :: thesis: |((B - A),(D - C))| = 0

consider x1, x2, y1, y2 being Element of REAL 2 such that

A4: L1 = Line (x1,x2) and

A5: L2 = Line (y1,y2) and

A6: x2 - x1 _|_ y2 - y1 by A1, EUCLIDLP:def 8;

A7: |((x2 - x1),(y2 - y1))| = 0 by A6, EUCLIDLP:def 3, RVSUM_1:def 17;

A8: ( A in Line (x1,x2) & B in Line (x1,x2) ) by A2, A4, EUCLID_4:41;

then consider lambda being Real such that

A9: A = ((1 - lambda) * x1) + (lambda * x2) ;

consider mu being Real such that

A10: B = ((1 - mu) * x1) + (mu * x2) by A8;

A11: ( C in Line (y1,y2) & D in Line (y1,y2) ) by A3, A5, EUCLID_4:41;

then consider lambda2 being Real such that

A12: C = ((1 - lambda2) * y1) + (lambda2 * y2) ;

consider mu2 being Real such that

A13: D = ((1 - mu2) * y1) + (mu2 * y2) by A11;

A14: B - A = (mu - lambda) * (x2 - x1) by A9, A10, Th1;

reconsider a = mu - lambda, b = mu2 - lambda2 as Real ;

|((B - A),(D - C))| = |((a * (x2 - x1)),(b * (y2 - y1)))| by A14, A12, A13, Th1

.= a * |((x2 - x1),(b * (y2 - y1)))| by EUCLID_4:21

.= a * (b * |((x2 - x1),(y2 - y1))|) by EUCLID_4:22

.= 0 by A7 ;

hence |((B - A),(D - C))| = 0 ; :: thesis: verum