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