let n be Nat; 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; 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; ( 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
; 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; verum