set Z2 = { (Class RK,a) where a is Element of G : Class RK,a in the carrier of (X ./. RK) } ;
set Z1 = union { (Class RK,a) where a is Element of G : Class RK,a in the carrier of (X ./. RK) } ;

A1: 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
A2: x in g and
A3: g in { (Class RK,a) where a is Element of G : Class RK,a in the carrier of (X ./. RK) } by TARSKI:def 4;
ex a being Element of G st
( g = Class RK,a & Class RK,a in the carrier of (X ./. RK) ) by A3;
hence x in the carrier of X by A2; :: thesis: verum

end;

0. X = 0. G by BCIALG_1:def 10;
then A4: Class RK,(0. X) in { (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 0. X in Class RK,(0. X) by EQREL_1:26;
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 A4, A1, TARSKI:def 3, TARSKI:def 4; :: thesis: verum