let A be non empty finite set ; :: thesis: for U being Function of (bool A),(bool A) st U . {} = {} & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds

ex R being non empty finite RelStr st

( the carrier of R = A & U = UAp R )

let L be Function of (bool A),(bool A); :: thesis: ( L . {} = {} & ( for X, Y being Subset of A holds L . (X \/ Y) = (L . X) \/ (L . Y) ) implies ex R being non empty finite RelStr st

( the carrier of R = A & L = UAp R ) )

assume that

A1: L . {} = {} and

A2: for X, Y being Subset of A holds L . (X \/ Y) = (L . X) \/ (L . Y) ; :: thesis: ex R being non empty finite RelStr st

( the carrier of R = A & L = UAp R )

defpred S_{1}[ set , set ] means $1 in L . {$2};

consider R being Relation of A such that

A3: for x, y being Element of A holds

( [x,y] in R iff S_{1}[x,y] )
from RELSET_1:sch 2();

reconsider RR = RelStr(# A,R #) as non empty finite RelStr ;

take RR ; :: thesis: ( the carrier of RR = A & L = UAp RR )

A4: for y being Element of RR

for Y being Subset of RR st Y = {y} holds

UAp Y = L . Y

then A11: dom (UAp RR) = dom L by FUNCT_2:def 1;

for x being object st x in dom (UAp RR) holds

(UAp RR) . x = L . x

ex R being non empty finite RelStr st

( the carrier of R = A & U = UAp R )

let L be Function of (bool A),(bool A); :: thesis: ( L . {} = {} & ( for X, Y being Subset of A holds L . (X \/ Y) = (L . X) \/ (L . Y) ) implies ex R being non empty finite RelStr st

( the carrier of R = A & L = UAp R ) )

assume that

A1: L . {} = {} and

A2: for X, Y being Subset of A holds L . (X \/ Y) = (L . X) \/ (L . Y) ; :: thesis: ex R being non empty finite RelStr st

( the carrier of R = A & L = UAp R )

defpred S

consider R being Relation of A such that

A3: for x, y being Element of A holds

( [x,y] in R iff S

reconsider RR = RelStr(# A,R #) as non empty finite RelStr ;

take RR ; :: thesis: ( the carrier of RR = A & L = UAp RR )

A4: for y being Element of RR

for Y being Subset of RR st Y = {y} holds

UAp Y = L . Y

proof

dom L = bool A
by FUNCT_2:def 1;
let y be Element of RR; :: thesis: for Y being Subset of RR st Y = {y} holds

UAp Y = L . Y

let Y be Subset of RR; :: thesis: ( Y = {y} implies UAp Y = L . Y )

assume A5: Y = {y} ; :: thesis: UAp Y = L . Y

thus UAp Y c= L . Y :: according to XBOOLE_0:def 10 :: thesis: L . Y c= UAp Y

assume A8: x in L . Y ; :: thesis: x in UAp Y

A9: y in Y by TARSKI:def 1, A5;

A10: L . Y in bool A by FUNCT_2:5;

then [x,y] in R by A3, A8, A5;

then y in Class (R,x) by EQREL_1:18;

then Class ( the InternalRel of RR,x) meets Y by A9, XBOOLE_0:3;

hence x in UAp Y by A10, A8; :: thesis: verum

end;UAp Y = L . Y

let Y be Subset of RR; :: thesis: ( Y = {y} implies UAp Y = L . Y )

assume A5: Y = {y} ; :: thesis: UAp Y = L . Y

thus UAp Y c= L . Y :: according to XBOOLE_0:def 10 :: thesis: L . Y c= UAp Y

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in L . Y or x in UAp Y )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in UAp Y or x in L . Y )

assume x in UAp Y ; :: thesis: x in L . Y

then consider a being Element of RR such that

A6: ( a = x & Class ( the InternalRel of RR,a) meets Y ) ;

consider z being object such that

A7: ( z in Class ( the InternalRel of RR,a) & z in Y ) by A6, XBOOLE_0:3;

z = y by A7, TARSKI:def 1, A5;

then [x,y] in R by A6, A7, EQREL_1:18;

hence x in L . Y by A5, A3, A6; :: thesis: verum

end;assume x in UAp Y ; :: thesis: x in L . Y

then consider a being Element of RR such that

A6: ( a = x & Class ( the InternalRel of RR,a) meets Y ) ;

consider z being object such that

A7: ( z in Class ( the InternalRel of RR,a) & z in Y ) by A6, XBOOLE_0:3;

z = y by A7, TARSKI:def 1, A5;

then [x,y] in R by A6, A7, EQREL_1:18;

hence x in L . Y by A5, A3, A6; :: thesis: verum

assume A8: x in L . Y ; :: thesis: x in UAp Y

A9: y in Y by TARSKI:def 1, A5;

A10: L . Y in bool A by FUNCT_2:5;

then [x,y] in R by A3, A8, A5;

then y in Class (R,x) by EQREL_1:18;

then Class ( the InternalRel of RR,x) meets Y by A9, XBOOLE_0:3;

hence x in UAp Y by A10, A8; :: thesis: verum

then A11: dom (UAp RR) = dom L by FUNCT_2:def 1;

for x being object st x in dom (UAp RR) holds

(UAp RR) . x = L . x

proof

hence
( the carrier of RR = A & L = UAp RR )
by A11, FUNCT_1:2; :: thesis: verum
let x be object ; :: thesis: ( x in dom (UAp RR) implies (UAp RR) . x = L . x )

assume A12: x in dom (UAp RR) ; :: thesis: (UAp RR) . x = L . x

end;assume A12: x in dom (UAp RR) ; :: thesis: (UAp RR) . x = L . x

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

end;

suppose
x <> {}
; :: thesis: (UAp RR) . x = L . x

then reconsider X = x as non empty finite Subset of RR by A12;

defpred S_{2}[ non empty finite Subset of RR] means (UAp RR) . $1 = L . $1;

A13: for x being Element of RR st x in X holds

S_{2}[{x}]

for B being non empty finite Subset of RR st x in X & B c= X & not x in B & S_{2}[B] holds

S_{2}[B \/ {x}]
_{2}[X]
from CHAIN_1:sch 2(A13, A14);

hence (UAp RR) . x = L . x ; :: thesis: verum

end;defpred S

A13: for x being Element of RR st x in X holds

S

proof

A14:
for x being Element of RR
let x be Element of RR; :: thesis: ( x in X implies S_{2}[{x}] )

assume x in X ; :: thesis: S_{2}[{x}]

set I = {x};

(UAp RR) . {x} = UAp {x} by Def11

.= L . {x} by A4 ;

hence S_{2}[{x}]
; :: thesis: verum

end;assume x in X ; :: thesis: S

set I = {x};

(UAp RR) . {x} = UAp {x} by Def11

.= L . {x} by A4 ;

hence S

for B being non empty finite Subset of RR st x in X & B c= X & not x in B & S

S

proof

S
let x be Element of RR; :: thesis: for B being non empty finite Subset of RR st x in X & B c= X & not x in B & S_{2}[B] holds

S_{2}[B \/ {x}]

let B be non empty finite Subset of RR; :: thesis: ( x in X & B c= X & not x in B & S_{2}[B] implies S_{2}[B \/ {x}] )

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

then A15: UAp B = L . B by Def11;

set I = {x};

(UAp RR) . (B \/ {x}) = UAp (B \/ {x}) by Def11

.= (UAp B) \/ (UAp {x}) by Th13

.= (L . B) \/ (L . {x}) by A4, A15

.= L . (B \/ {x}) by A2 ;

hence S_{2}[B \/ {x}]
; :: thesis: verum

end;S

let B be non empty finite Subset of RR; :: thesis: ( x in X & B c= X & not x in B & S

assume ( x in X & B c= X & not x in B & S

then A15: UAp B = L . B by Def11;

set I = {x};

(UAp RR) . (B \/ {x}) = UAp (B \/ {x}) by Def11

.= (UAp B) \/ (UAp {x}) by Th13

.= (L . B) \/ (L . {x}) by A4, A15

.= L . (B \/ {x}) by A2 ;

hence S

hence (UAp RR) . x = L . x ; :: thesis: verum