let POS be OrtAfSp; :: thesis: for b, c, a being Element of POS holds
( b,c _|_ a,a & a,a _|_ b,c & b,c // a,a & a,a // b,c )
let b, c, a 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 (Af POS) ;
thus b,c _|_ a,a by Def9; :: thesis: ( a,a _|_ b,c & b,c // a,a & a,a // b,c )
hence a,a _|_ b,c by Def9; :: 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 Th48; :: thesis: verum