let n be Nat; :: thesis: for x0, x1, y0, y1 being Element of REAL n
for L1, L2 being Element of line_of_REAL n st x0 in L1 & x1 in L1 & x0 <> x1 & y0 in L2 & y1 in L2 & y0 <> y1 & L1 _|_ L2 holds
x1 - x0 _|_ y1 - y0
let x0, x1, y0, y1 be Element of REAL n; :: thesis: for L1, L2 being Element of line_of_REAL n st x0 in L1 & x1 in L1 & x0 <> x1 & y0 in L2 & y1 in L2 & y0 <> y1 & L1 _|_ L2 holds
x1 - x0 _|_ y1 - y0
let L1, L2 be Element of line_of_REAL n; :: thesis: ( x0 in L1 & x1 in L1 & x0 <> x1 & y0 in L2 & y1 in L2 & y0 <> y1 & L1 _|_ L2 implies x1 - x0 _|_ y1 - y0 )
assume that
A1: ( x0 in L1 & x1 in L1 ) and
A2: x0 <> x1 and
A3: ( y0 in L2 & y1 in L2 ) and
A4: y0 <> y1 and
A5: L1 _|_ L2 ; :: thesis: x1 - x0 _|_ y1 - y0
consider x2, x3, y2, y3 being Element of REAL n such that
A6: L1 = Line (x2,x3) and
A7: L2 = Line (y2,y3) and
A8: x3 - x2 _|_ y3 - y2 by A5;
consider s being Real such that
A9: x1 - x0 = s * (x3 - x2) by A1, A6, Th31;
x3 - x2,y3 - y2 are_orthogonal by A8;
then A10: |((x3 - x2),(y3 - y2))| = 0 by RVSUM_1:def 17;
consider t being Real such that
A11: y1 - y0 = t * (y3 - y2) by A3, A7, Th31;
|((x1 - x0),(y1 - y0))| = s * |((x3 - x2),(y1 - y0))| by A9, EUCLID_4:21
.= s * (t * |((x3 - x2),(y3 - y2))|) by A11, EUCLID_4:22
.= 0 by A10 ;
then A12: x1 - x0,y1 - y0 are_orthogonal by RVSUM_1:def 17;
( x1 - x0 <> 0* n & y1 - y0 <> 0* n ) by A2, A4, Th9;
hence x1 - x0 _|_ y1 - y0 by A12; :: thesis: verum