let OAS be OAffinSpace; :: thesis: for a, b, c being Element of OAS
for a', b', c' being Element of (Lambda OAS) st a = a' & b = b' & c = c' holds
( LIN a,b,c iff LIN a',b',c' )
let a, b, c be Element of OAS; :: thesis: for a', b', c' being Element of (Lambda OAS) st a = a' & b = b' & c = c' holds
( LIN a,b,c iff LIN a',b',c' )
let a', b', c' be Element of (Lambda OAS); :: thesis: ( a = a' & b = b' & c = c' implies ( LIN a,b,c iff LIN a',b',c' ) )
assume A1: ( a = a' & b = b' & c = c' ) ; :: thesis: ( LIN a,b,c iff LIN a',b',c' )

A2: now

assume LIN a',b',c' ; :: thesis: LIN a,b,c
then a',b' // a',c' 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;

now

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

end;

hence ( LIN a,b,c iff LIN a',b',c' ) by A2; :: thesis: verum