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