let A be non empty finite set ; :: thesis: for L, H being Function of (bool A),(bool A) st L = Flip H holds
( ( H . {} = {} & ( for X, Y being Subset of A holds H . (X \/ Y) = (H . X) \/ (H . Y) ) ) iff ex R being non empty finite RelStr st
( the carrier of R = A & LAp R = L & UAp R = H & ( for x, y being Element of R holds
( [x,y] in the InternalRel of R iff x in H . {y} ) ) ) )
let L, H be Function of (bool A),(bool A); :: thesis: ( L = Flip H implies ( ( H . {} = {} & ( for X, Y being Subset of A holds H . (X \/ Y) = (H . X) \/ (H . Y) ) ) iff ex R being non empty finite RelStr st
( the carrier of R = A & LAp R = L & UAp R = H & ( for x, y being Element of R holds
( [x,y] in the InternalRel of R iff x in H . {y} ) ) ) ) )
assume ZA: L = Flip H ; :: thesis: ( ( H . {} = {} & ( for X, Y being Subset of A holds H . (X \/ Y) = (H . X) \/ (H . Y) ) ) iff ex R being non empty finite RelStr st
( the carrier of R = A & LAp R = L & UAp R = H & ( for x, y being Element of R holds
( [x,y] in the InternalRel of R iff x in H . {y} ) ) ) )
thus ( H . {} = {} & ( for X, Y being Subset of A holds H . (X \/ Y) = (H . X) \/ (H . Y) ) implies ex R being non empty finite RelStr st
( the carrier of R = A & LAp R = L & UAp R = H & ( for x, y being Element of R holds
( [x,y] in the InternalRel of R iff x in H . {y} ) ) ) ) :: thesis: ( ex R being non empty finite RelStr st
( the carrier of R = A & LAp R = L & UAp R = H & ( for x, y being Element of R holds
( [x,y] in the InternalRel of R iff x in H . {y} ) ) ) implies ( H . {} = {} & ( for X, Y being Subset of A holds H . (X \/ Y) = (H . X) \/ (H . Y) ) ) )
proof
assume A0: ( H . {} = {} & ( for X, Y being Subset of A holds H . (X \/ Y) = (H . X) \/ (H . Y) ) ) ; :: thesis: ex R being non empty finite RelStr st
( the carrier of R = A & LAp R = L & UAp R = H & ( for x, y being Element of R holds
( [x,y] in the InternalRel of R iff x in H . {y} ) ) )
defpred S1[ set , set ] means $1 in H . {$2};
consider R being Relation of A such that
WW1: for x, y being Element of A holds
( [x,y] in R iff S1[x,y] ) from RELSET_1:sch 2();
 set RR = RelStr(# A,R #);
reconsider RR = RelStr(# A,R #) as non empty finite RelStr ;
W1: for X being Subset of RR holds (UAp RR) . X = H . X
proof
let X be Subset of RR; :: thesis: (UAp RR) . X = H . X
deffunc H1() -> set = the carrier of RR;
defpred S2[ set ] means for X being Subset of RR st X c= $1 holds
(UAp RR) . X = H . X;
U1: the carrier of RR is finite ;
for X being Subset of RR st X c= {} holds
(UAp RR) . X = H . X
proof
let X be Subset of RR; :: thesis: ( X c= {} implies (UAp RR) . X = H . X )
F2: UAp ({} RR) = {} ;
assume X c= {} ; :: thesis: (UAp RR) . X = H . X
then X = {} ;
hence (UAp RR) . X = H . X by ROUGHS_2:def 11, F2, A0; :: thesis: verum
end;
then U2: S2[ {} ] ;
U3: for x, B being set st x in H1() & B c= H1() & S2[B] holds
S2[B \/ {x}]
proof
let x, B be set ; :: thesis: ( x in H1() & B c= H1() & S2[B] implies S2[B \/ {x}] )
assume I1: ( x in H1() & B c= H1() & S2[B] ) ; :: thesis: S2[B \/ {x}]
BE: H . {x} = { y where y is Element of RR : x in Class ( the InternalRel of RR,y) }
proof
thus H . {x} c= { y where y is Element of RR : x in Class ( the InternalRel of RR,y) } :: according to XBOOLE_0:def 10 :: thesis: { y where y is Element of RR : x in Class ( the InternalRel of RR,y) } c= H . {x}
proof
let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in H . {x} or w in { y where y is Element of RR : x in Class ( the InternalRel of RR,y) } )
assume P1: w in H . {x} ; :: thesis: w in { y where y is Element of RR : x in Class ( the InternalRel of RR,y) }
{x} c= A by I1, ZFMISC_1:31;
then t1: H . {x} in bool A by FUNCT_2:5;
reconsider xxx = x as Element of A by I1;
reconsider www = w as Element of RR by t1, P1;
P2: [www,xxx] in the InternalRel of RR by WW1, P1;
www in {www} by TARSKI:def 1;
then x in Class ( the InternalRel of RR,www) by P2, RELAT_1:def 13;
hence w in { y where y is Element of RR : x in Class ( the InternalRel of RR,y) } ; :: thesis: verum
end;
let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in { y where y is Element of RR : x in Class ( the InternalRel of RR,y) } or w in H . {x} )
assume w in { y where y is Element of RR : x in Class ( the InternalRel of RR,y) } ; :: thesis: w in H . {x}
then consider ww being Element of RR such that
P3: ( ww = w & x in Class ( the InternalRel of RR,ww) ) ;
consider xx being object such that
P4: ( [xx,x] in the InternalRel of RR & xx in {ww} ) by P3, RELAT_1:def 13;
xx = ww by P4, TARSKI:def 1;
hence w in H . {x} by WW1, P3, P4; :: thesis: verum
end;
reconsider xx = {x} as Subset of RR by I1, ZFMISC_1:31;
WX: { y where y is Element of RR : Class ( the InternalRel of RR,y) meets xx } = { y where y is Element of RR : x in Class ( the InternalRel of RR,y) }
proof
thus { y where y is Element of RR : Class ( the InternalRel of RR,y) meets xx } c= { y where y is Element of RR : x in Class ( the InternalRel of RR,y) } :: according to XBOOLE_0:def 10 :: thesis: { y where y is Element of RR : x in Class ( the InternalRel of RR,y) } c= { y where y is Element of RR : Class ( the InternalRel of RR,y) meets xx }
proof
let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in { y where y is Element of RR : Class ( the InternalRel of RR,y) meets xx } or w in { y where y is Element of RR : x in Class ( the InternalRel of RR,y) } )
assume w in { y where y is Element of RR : Class ( the InternalRel of RR,y) meets xx } ; :: thesis: w in { y where y is Element of RR : x in Class ( the InternalRel of RR,y) }
then consider ww being Element of RR such that
H1: ( ww = w & Class ( the InternalRel of RR,ww) meets xx ) ;
x in Class ( the InternalRel of RR,ww) by H1, ZFMISC_1:50;
hence w in { y where y is Element of RR : x in Class ( the InternalRel of RR,y) } by H1; :: thesis: verum
end;
let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in { y where y is Element of RR : x in Class ( the InternalRel of RR,y) } or w in { y where y is Element of RR : Class ( the InternalRel of RR,y) meets xx } )
assume w in { y where y is Element of RR : x in Class ( the InternalRel of RR,y) } ; :: thesis: w in { y where y is Element of RR : Class ( the InternalRel of RR,y) meets xx }
then consider ww being Element of RR such that
H1: ( ww = w & x in Class ( the InternalRel of RR,ww) ) ;
Class ( the InternalRel of RR,ww) meets xx by H1, ZFMISC_1:48;
hence w in { y where y is Element of RR : Class ( the InternalRel of RR,y) meets xx } by H1; :: thesis: verum
end;
for X being Subset of RR st X c= B \/ {x} holds
(UAp RR) . X = H . X
proof
let X be Subset of RR; :: thesis: ( X c= B \/ {x} implies (UAp RR) . X = H . X )
assume WW: X c= B \/ {x} ; :: thesis: (UAp RR) . X = H . X
X \ {x} c= (B \/ {x}) \ {x} by WW, XBOOLE_1:33;
then W8: X \ {x} c= B \ {x} by XBOOLE_1:40;
per cases ( x in X or not x in X ) ;
suppose XX1: x in X ; :: thesis: (UAp RR) . X = H . X
reconsider XX = X \ {x} as Subset of RR ;
Ji: XX \/ xx = X by XX1, ZFMISC_1:116;
OP: UAp xx = H . xx by BE, WX, ROUGHS_1:def 5;
OR: H . XX = (UAp RR) . XX by W8, XBOOLE_1:1, I1
.= UAp XX by ROUGHS_2:def 11 ;
(UAp RR) . X = UAp X by ROUGHS_2:def 11
.= (UAp XX) \/ (UAp xx) by ROUGHS_2:13, Ji
.= H . X by A0, Ji, OP, OR ;
hence (UAp RR) . X = H . X ; :: thesis: verum
end;
suppose not x in X ; :: thesis: (UAp RR) . X = H . X
hence (UAp RR) . X = H . X by I1, ZFMISC_1:135, WW; :: thesis: verum
end;
end;
end;
hence S2[B \/ {x}] ; :: thesis: verum
end;
S2[ the carrier of RR] from FINSET_1:sch 2(U1, U2, U3);
 hence (UAp RR) . X = H . X ; :: thesis: verum
end;
T3: UAp RR = H by W1, FUNCT_2:63;
then LAp RR = L by ROUGHS_2:27, ZA;
hence ex R being non empty finite RelStr st
( the carrier of R = A & LAp R = L & UAp R = H & ( for x, y being Element of R holds
( [x,y] in the InternalRel of R iff x in H . {y} ) ) ) by T3, WW1; :: thesis: verum
end;
given R being non empty finite RelStr such that U0: ( the carrier of R = A & LAp R = L & UAp R = H & ( for x, y being Element of R holds
( [x,y] in the InternalRel of R iff x in H . {y} ) ) ) ; :: thesis: ( H . {} = {} & ( for X, Y being Subset of A holds H . (X \/ Y) = (H . X) \/ (H . Y) ) )
thus ( H . {} = {} & ( for X, Y being Subset of A holds H . (X \/ Y) = (H . X) \/ (H . Y) ) ) by UApAdditive, U0, UApEmpty; :: thesis: verum