let X be OrtAfPl; :: thesis: for a, b, c being Element of X

for A being Subset of X st A is being_line & a in A & b in A & c in A holds

LIN a,b,c

let a, b, c be Element of X; :: thesis: for A being Subset of X st A is being_line & a in A & b in A & c in A holds

LIN a,b,c

let A be Subset of X; :: thesis: ( A is being_line & a in A & b in A & c in A implies LIN a,b,c )

assume that

A1: A is being_line and

A2: a in A and

A3: b in A and

A4: c in A ; :: thesis: LIN a,b,c

reconsider a9 = a, b9 = b, c9 = c as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

reconsider A9 = A as Subset of AffinStruct(# the carrier of X, the CONGR of X #) ;

A9 is being_line by A1, ANALMETR:43;

then LIN a9,b9,c9 by A2, A3, A4, AFF_1:21;

hence LIN a,b,c by ANALMETR:40; :: thesis: verum

for A being Subset of X st A is being_line & a in A & b in A & c in A holds

LIN a,b,c

let a, b, c be Element of X; :: thesis: for A being Subset of X st A is being_line & a in A & b in A & c in A holds

LIN a,b,c

let A be Subset of X; :: thesis: ( A is being_line & a in A & b in A & c in A implies LIN a,b,c )

assume that

A1: A is being_line and

A2: a in A and

A3: b in A and

A4: c in A ; :: thesis: LIN a,b,c

reconsider a9 = a, b9 = b, c9 = c as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

reconsider A9 = A as Subset of AffinStruct(# the carrier of X, the CONGR of X #) ;

A9 is being_line by A1, ANALMETR:43;

then LIN a9,b9,c9 by A2, A3, A4, AFF_1:21;

hence LIN a,b,c by ANALMETR:40; :: thesis: verum