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 :: thesis: for x being object st x in union { (Class (RK,a)) where a is Element of G : Class (RK,a) in the carrier of (X ./. RK) } holds
x in the carrier of X

let x be object ; :: 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:5;
then 0. X in Class (RK,(0. X)) by EQREL_1:18;
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