let a, b, c, d be Element of the WeakAffVect; :: thesis: for a9, b9, c9, d9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a = a9 & b = b9 & c = c9 & d = d9 holds
( a,b '||' c,d iff a9,b9 // c9,d9 )
let a9, b9, c9, d9 be Element of AffinStruct(# the carrier of the WeakAffVect,P #); :: thesis: ( a = a9 & b = b9 & c = c9 & d = d9 implies ( a,b '||' c,d iff a9,b9 // c9,d9 ) )
assume A1: ( a = a9 & b = b9 & c = c9 & d = d9 ) ; :: thesis: ( a,b '||' c,d iff a9,b9 // c9,d9 )
A2: now :: thesis: ( a9,b9 // c9,d9 implies a,b '||' c,d )
assume a9,b9 // c9,d9 ; :: thesis: a,b '||' c,d
then [[a9,b9],[c9,d9]] in P by ANALOAF:def 2;
hence a,b '||' c,d by A1, Lm14; :: thesis: verum
end;
now :: thesis: ( a,b '||' c,d implies a9,b9 // c9,d9 )
assume a,b '||' c,d ; :: thesis: a9,b9 // c9,d9
then [[a,b],[c,d]] in the CONGR of AffinStruct(# the carrier of the WeakAffVect,P #) by Lm14;
hence a9,b9 // c9,d9 by A1, ANALOAF:def 2; :: thesis: verum
end;
hence ( a,b '||' c,d iff a9,b9 // c9,d9 ) by A2; :: thesis: verum