let OAS be OAffinSpace; :: thesis: for a, b, c being Element of OAS
for a9, b9, c9 being Element of (Lambda OAS) st a = a9 & b = b9 & c = c9 holds
( LIN a,b,c iff LIN a9,b9,c9 )
let a, b, c be Element of OAS; :: thesis: for a9, b9, c9 being Element of (Lambda OAS) st a = a9 & b = b9 & c = c9 holds
( LIN a,b,c iff LIN a9,b9,c9 )
let a9, b9, c9 be Element of (Lambda OAS); :: 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 )

A2: now

assume LIN a,b,c ; :: thesis: LIN a9,b9,c9
then a,b '||' a,c by DIRAF:def 5;
then a9,b9 // a9,c9 by A1, DIRAF:45;
hence LIN a9,b9,c9 by AFF_1:def 1; :: thesis: verum

end;

now

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, DIRAF:45;
hence LIN a,b,c by DIRAF:def 5; :: thesis: verum

end;

hence ( LIN a,b,c iff LIN a9,b9,c9 ) by A2; :: thesis: verum