let A be Subset of (dom H); :: thesis:

end;

assume union A in dom H ; :: thesis:
reconsider AA = A as Element of Fin (bool the carrier of R) by K1, FINSUB_1:def 5;
reconsider HH = H as Function of (bool the carrier of R),(Fin the carrier of R) by FINSUB_1:14;
defpred S₁[ Subset of (bool the carrier of R)] means H . (union $1) = union (H .: $1);
V1: for x being Element of bool the carrier of R holds S₁[{x}]

let x be Element of bool the carrier of R; :: thesis:
H . (union {x}) = H . x by ZFMISC_1:25
.= union {(H . x)} by ZFMISC_1:25
.= union (Im (H,x)) by K1, FUNCT_1:59
.= union (H .: {x}) ;
hence S₁[{x}] ; :: thesis:

end;

V2: for B1, B2 being non empty Subset of (bool the carrier of R) st S₁[B1] & S₁[B2] holds
S₁[B1 \/ B2]

let B1, B2 be non empty Subset of (bool the carrier of R); :: thesis:
assume BB: ( S₁[B1] & S₁[B2] ) ; :: thesis:
set B12 = B1 \/ B2;
zx: for g being set st g in B1 holds
g c= the carrier of R ;
for g being set st g in B2 holds
g c= the carrier of R ;
then reconsider U1 = union B1, U2 = union B2 as Subset of R by zx, ZFMISC_1:76;
H . (union (B1 \/ B2)) = H . ((union B1) \/ (union B2)) by ZFMISC_1:78
.= (H . U1) \/ (H . U2) by ROUGHS_4:def 9, AA
.= union ((H .: B1) \/ (H .: B2)) by ZFMISC_1:78, BB
.= union (H .: (B1 \/ B2)) by RELAT_1:120 ;
hence S₁[B1 \/ B2] ; :: thesis:

end;

SS: for B being non empty Subset of (bool the carrier of R) holds S₁[B] from ROUGHS_3:sch 2(V1, V2);
reconsider AA = A as non empty Subset of (bool the carrier of R) by KJ, FUNCT_2:def 1;
H . (union AA) = union (H .: AA) by SS;
hence H . (union A) = union (H .: A) ; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume a1: x in (UAp (GeneratedRelStr H)) . X ; :: thesis:
reconsider XX = X as Subset of (GeneratedRelStr H) ;
a2: x in UAp XX by ROUGHS_2:def 11, a1;
reconsider xx = x as Element of R by a2;
consider y being object such that
a4: ( y in Class ((GeneratedRelation (R,H)),x) & y in X ) by a2, XBOOLE_0:3, ROUGHS_2:7;
reconsider y = y as Element of R by a4;
reconsider Y = {y} as Subset of R ;
[xx,y] in GeneratedRelation (R,H) by RELSET_2:9, a4;
then a5: xx in H . {y} by GRDef;
H . Y c= H . X by AA, ROUGHS_4:def 8, a4, ZFMISC_1:31;
hence x in H . X by a5; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume a1: x in H . X ; :: thesis:
reconsider XX = X as Subset of (GeneratedRelStr H) ;
consider y being set such that
b1: ( y in X & x in H . {y} ) by a1, KeyLemma, g2, K1, COHSP_1:def 9;
reconsider xx = x as Element of R by a1;
reconsider Y = {y} as Subset of R by b1, ZFMISC_1:31;
reconsider xx = x, yy = y as Element of R by a1, b1;
[xx,yy] in GeneratedRelation (R,H) by GRDef, b1;
then ( yy in Class ((GeneratedRelation (R,H)),xx) & y in XX ) by b1, RELSET_2:9;
then Class ( the InternalRel of (GeneratedRelStr H),xx) meets XX by XBOOLE_0:3;
then xx in { x where x is Element of (GeneratedRelStr H) : Class ( the InternalRel of (GeneratedRelStr H),x) meets XX } ;
then xx in UAp XX by ROUGHS_1:def 5;
hence x in (UAp (GeneratedRelStr H)) . X by ROUGHS_2:def 11; :: thesis:

end;

end;