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