let n be Nat; for An, Bn, Cn being Point of (TOP-REAL n)
for L1, L2 being Element of line_of_REAL n st An <> Bn & An <> Cn & |((An - Bn),(An - Cn))| = 0 & L1 = Line (An,Bn) & L2 = Line (An,Cn) holds
L1 _|_ L2
let An, Bn, Cn be Point of (TOP-REAL n); for L1, L2 being Element of line_of_REAL n st An <> Bn & An <> Cn & |((An - Bn),(An - Cn))| = 0 & L1 = Line (An,Bn) & L2 = Line (An,Cn) holds
L1 _|_ L2
let L1, L2 be Element of line_of_REAL n; ( An <> Bn & An <> Cn & |((An - Bn),(An - Cn))| = 0 & L1 = Line (An,Bn) & L2 = Line (An,Cn) implies L1 _|_ L2 )
assume that
A1:
An <> Bn
and
A2:
An <> Cn
and
A3:
|((An - Bn),(An - Cn))| = 0
and
A4:
L1 = Line (An,Bn)
and
A5:
L2 = Line (An,Cn)
; L1 _|_ L2
reconsider rA = An, rB = Bn, rC = Cn as Element of REAL n by EUCLID:22;
A6:
L1 = Line (rA,rB)
by A4, EUCLID12:4;
A7:
L2 = Line (rA,rC)
by A5, EUCLID12:4;
A8:
rA - rB <> 0* n
by A1, EUCLIDLP:9;
A9:
rA - rC <> 0* n
by A2, EUCLIDLP:9;
rA - rB _|_ rA - rC
by A8, A9, EUCLIDLP:def 3, A3, RVSUM_1:def 17;
hence
L1 _|_ L2
by A6, A7, EUCLIDLP:def 8; verum