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) ) ) )

( [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

( ( 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

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
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 S_{1}[ 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 S_{1}[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

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;( 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 S

consider R being Relation of A such that

WW1: for x, y being Element of A holds

( [x,y] in R iff S

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

T3:
UAp RR = H
by W1, FUNCT_2:63;
let X be Subset of RR; :: thesis: (UAp RR) . X = H . X

deffunc H_{1}() -> set = the carrier of RR;

defpred S_{2}[ 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_{2}[ {} ]
;

U3: for x, B being set st x in H_{1}() & B c= H_{1}() & S_{2}[B] holds

S_{2}[B \/ {x}]
_{2}[ the carrier of RR]
from FINSET_1:sch 2(U1, U2, U3);

hence (UAp RR) . X = H . X ; :: thesis: verum

end;deffunc H

defpred S

(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

then U2:
S
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;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

U3: for x, B being set st x in H

S

proof

S
let x, B be set ; :: thesis: ( x in H_{1}() & B c= H_{1}() & S_{2}[B] implies S_{2}[B \/ {x}] )

assume I1: ( x in H_{1}() & B c= H_{1}() & S_{2}[B] )
; :: thesis: S_{2}[B \/ {x}]

BE: H . {x} = { y where y is Element of RR : x in Class ( the InternalRel of RR,y) }

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) }

(UAp RR) . X = H . X_{2}[B \/ {x}]
; :: thesis: verum

end;assume I1: ( x in H

BE: H . {x} = { y where y is Element of RR : x in Class ( the InternalRel of RR,y) }

proof

reconsider xx = {x} as Subset of RR by I1, ZFMISC_1:31;
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}

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

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} )
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;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

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

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

for X being Subset of RR st X c= B \/ {x} holds
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 }

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

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 } )
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;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

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

(UAp RR) . X = H . X

proof

hence
S
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;

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

end;

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

hence (UAp RR) . X = H . X ; :: thesis: verum

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

( [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