set Z1 = union { (Class RK,a) where a is Element of G : Class RK,a in the carrier of (X ./. RK) } ;
set Z2 = { (Class RK,a) where a is Element of G : Class RK,a in the carrier of (X ./. RK) } ;
[(0. X),(0. X)] in RK by EQREL_1:11;
then B5: 0. X in Class RK,(0. X) by EQREL_1:26;
0. X = 0. G by BCIALG_1:def 10;
then a1: Class RK,(0. X) in { (Class RK,a) where a is Element of G : Class RK,a in the carrier of (X ./. RK) } ;

now

let x be set ; :: thesis: ( x in union { (Class RK,a) where a is Element of G : Class RK,a in the carrier of (X ./. RK) } implies x in the carrier of X )
assume x in union { (Class RK,a) where a is Element of G : Class RK,a in the carrier of (X ./. RK) } ; :: thesis: x in the carrier of X
then consider g being set such that
A1: ( x in g & g in { (Class RK,a) where a is Element of G : Class RK,a in the carrier of (X ./. RK) } ) by TARSKI:def 4;
consider a being Element of G such that
A3: ( g = Class RK,a & Class RK,a in the carrier of (X ./. RK) ) by A1;
thus x in the carrier of X by A1, A3; :: thesis: verum

end;

hence union { (Class RK,a) where a is Element of G : Class RK,a in the carrier of (X ./. RK) } is non empty Subset of X by a1, B5, TARSKI:def 3, TARSKI:def 4; :: thesis: verum