let n be Nat; for A, C being Subset of (REAL n)
for x1, x2 being Element of REAL n st A is being_line & C is being_line & x1 in A & x2 in A & x1 in C & x2 in C & not x1 = x2 holds
A = C
let A, C be Subset of (REAL n); for x1, x2 being Element of REAL n st A is being_line & C is being_line & x1 in A & x2 in A & x1 in C & x2 in C & not x1 = x2 holds
A = C
let x1, x2 be Element of REAL n; ( A is being_line & C is being_line & x1 in A & x2 in A & x1 in C & x2 in C & not x1 = x2 implies A = C )
assume that
A1:
A is being_line
and
A2:
C is being_line
and
A3:
( x1 in A & x2 in A )
and
A4:
( x1 in C & x2 in C )
; ( x1 = x2 or A = C )
assume A5:
x1 <> x2
; A = C
then
A = Line (x1,x2)
by A1, A3, Lm3;
hence
A = C
by A2, A4, A5, Lm3; verum