let POS be OrtAfSp; :: thesis: for b, c, a being Element of holds
( b,c _|_ a,a & a,a _|_ b,c & b,c // a,a & a,a // b,c )
let b, c, a be Element of ; :: thesis: ( b,c _|_ a,a & a,a _|_ b,c & b,c // a,a & a,a // b,c )
reconsider a' = a, b' = b, c' = c as Element of ;
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 )
( b',c' // a',a' & a',a' // b',c' ) by AFF_1:12;
hence ( b,c // a,a & a,a // b,c ) by Th48; :: thesis: verum