let POS be OrtAfSp; :: thesis: for a, b, c being Element of POS
for a9, b9, c9 being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) st a = a9 & b = b9 & c = c9 holds
( LIN a,b,c iff LIN a9,b9,c9 )
let a, b, c be Element of POS; :: thesis: for a9, b9, c9 being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) st a = a9 & b = b9 & c = c9 holds
( LIN a,b,c iff LIN a9,b9,c9 )
let a9, b9, c9 be Element of AffinStruct(# the carrier of POS, the CONGR of POS #); :: thesis: ( a = a9 & b = b9 & c = c9 implies ( LIN a,b,c iff LIN a9,b9,c9 ) )
assume A1: ( a = a9 & b = b9 & c = c9 ) ; :: thesis: ( LIN a,b,c iff LIN a9,b9,c9 )

hereby :: thesis: ( LIN a9,b9,c9 implies LIN a,b,c )

assume LIN a,b,c ; :: thesis: LIN a9,b9,c9
then a,b // a,c ;
then a9,b9 // a9,c9 by A1, Th36;
hence LIN a9,b9,c9 by AFF_1:def 1; :: thesis: verum

end;

assume LIN a9,b9,c9 ; :: thesis: LIN a,b,c
then a9,b9 // a9,c9 by AFF_1:def 1;
then a,b // a,c by A1, Th36;
hence LIN a,b,c ; :: thesis: verum