A1: 0. G = 0. X by BCIALG_1:def 10;
then ( 0. G in Class RK,(0. G) & Class RK,(0. G) in { (Class RK,c) where c is Element of G : Class RK,c in the carrier of (X ./. RK) } ) by EQREL_1:28;
hence 0. X is Element of Union G,RK by A1, TARSKI:def 4; :: thesis: verum