let POS be OrtAfSp; :: thesis: for a, b, c being Element of POS
for a', b', c' being Element of (Af POS) st a = a' & b = b' & c = c' holds
( LIN a,b,c iff LIN a',b',c' )
let a, b, c be Element of POS; :: thesis: for a', b', c' being Element of (Af POS) st a = a' & b = b' & c = c' holds
( LIN a,b,c iff LIN a',b',c' )
let a', b', c' be Element of (Af POS); :: 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' )

hereby :: thesis: ( LIN a',b',c' implies LIN a,b,c )

assume LIN a,b,c ; :: thesis: LIN a',b',c'
then a,b // a,c by Def11;
then a',b' // a',c' by A1, Th48;
hence LIN a',b',c' by AFF_1:def 1; :: thesis: verum

end;

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, Th48;
hence LIN a,b,c by Def11; :: thesis: verum