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)

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

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

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

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

end;

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_{1}[ 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_{1}[{x}]
_{1}[B1] & S_{1}[B2] holds

S_{1}[B1 \/ B2]
_{1}[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;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

V1: for x being Element of bool the carrier of R holds S

proof

V2:
for B1, B2 being non empty Subset of (bool the carrier of R) st S
let x be Element of bool the carrier of R; :: thesis: S_{1}[{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_{1}[{x}]
; :: thesis: verum

end;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

S

proof

SS:
for B being non empty Subset of (bool the carrier of R) holds S
let B1, B2 be non empty Subset of (bool the carrier of R); :: thesis: ( S_{1}[B1] & S_{1}[B2] implies S_{1}[B1 \/ B2] )

assume BB: ( S_{1}[B1] & S_{1}[B2] )
; :: thesis: S_{1}[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_{1}[B1 \/ B2]
; :: thesis: verum

end;assume BB: ( S

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

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

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

proof

hence
UAp (GeneratedRelStr H) = H
by FUNCT_2:63; :: thesis: verum
let X be Subset of R; :: thesis: (UAp (GeneratedRelStr H)) . X = H . X

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

end;PS: (UAp (GeneratedRelStr H)) . X c= H . X

proof

H . X c= (UAp (GeneratedRelStr H)) . X
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;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

proof

hence
(UAp (GeneratedRelStr H)) . X = H . X
by XBOOLE_0:def 10, PS; :: thesis: verum
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;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