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:20;
hence 0. X is Element of Union (G,RK) by A1, TARSKI:def 4; :: thesis: verum