take kappa R ; :: thesis: ( kappa R is satisfying_RIF1 & kappa R is satisfying_RIF2 )
thus ( kappa R is satisfying_RIF1 & kappa R is satisfying_RIF2 ) ; :: thesis: verum