let R be non empty finite RelStr ; :: thesis: for H being Function of (bool the carrier of R),(bool the carrier of R) st H . {} = {} & H is \/-preserving holds
UAp (GeneratedRelStr H) = H
let H be Function of (bool the carrier of R),(bool the carrier of R); :: thesis: ( H . {} = {} & H is \/-preserving implies UAp (GeneratedRelStr H) = H )
assume AA: ( H . {} = {} & H is \/-preserving ) ; :: thesis: UAp (GeneratedRelStr H) = H
K1: dom H = bool the carrier of R by FUNCT_2:def 1;
g2: for A being Subset of (dom H) st union A in dom H holds
H . (union A) = union (H .: A)

proof

let A be Subset of (dom H); :: thesis: ( union A in dom H implies H . (union A) = union (H .: A) )

per cases ( A = {} or A <> {} ) ;

suppose A = {} ; :: thesis: ( union A in dom H implies H . (union A) = union (H .: A) )

hence ( union A in dom H implies H . (union A) = union (H .: A) ) by AA, ZFMISC_1:2; :: thesis: verum

end;

suppose KJ: A <> {} ; :: thesis: ( union A in dom H implies H . (union A) = union (H .: A) )

assume union A in dom H ; :: thesis: H . (union A) = union (H .: A)
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}]

proof

let x be Element of bool the carrier of R; :: thesis: S₁[{x}]
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: verum

end;

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

proof

let B1, B2 be non empty Subset of (bool the carrier of R); :: thesis: ( S₁[B1] & S₁[B2] implies S₁[B1 \/ B2] )
assume BB: ( S₁[B1] & S₁[B2] ) ; :: thesis: S₁[B1 \/ B2]
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: verum

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: verum

end;

end;

end;

set HH = UAp (GeneratedRelStr H);
for X being Subset of R holds (UAp (GeneratedRelStr H)) . X = H . X

proof

let X be Subset of R; :: thesis: (UAp (GeneratedRelStr H)) . X = H . X
PS: (UAp (GeneratedRelStr H)) . X c= H . X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (UAp (GeneratedRelStr H)) . X or x in H . X )
assume a1: x in (UAp (GeneratedRelStr H)) . X ; :: thesis: x in H . X
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: verum

end;

H . X c= (UAp (GeneratedRelStr H)) . X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H . X or x in (UAp (GeneratedRelStr H)) . X )
assume a1: x in H . X ; :: thesis: x in (UAp (GeneratedRelStr H)) . X
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: verum

end;

hence (UAp (GeneratedRelStr H)) . X = H . X by XBOOLE_0:def 10, PS; :: thesis: verum

end;

hence UAp (GeneratedRelStr H) = H by FUNCT_2:63; :: thesis: verum