let POS be OrtAfSp; :: thesis: for a, b, c being Element of POS holds
( b,c _|_ a,a & a,a _|_ b,c & b,c // a,a & a,a // b,c )
let a, b, c be Element of POS; :: thesis: ( b,c _|_ a,a & a,a _|_ b,c & b,c // a,a & a,a // b,c )
reconsider a9 = a, b9 = b, c9 = c as Element of AffinStruct(# the carrier of POS, the CONGR of POS #) ;
thus b,c _|_ a,a by Def7; :: thesis: ( a,a _|_ b,c & b,c // a,a & a,a // b,c )
hence a,a _|_ b,c by Def7; :: thesis: ( b,c // a,a & a,a // b,c )
( b9,c9 // a9,a9 & a9,a9 // b9,c9 ) by AFF_1:3;
hence ( b,c // a,a & a,a // b,c ) by Th36; :: thesis: verum