let A be non empty finite set ; 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); ( 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
; ( ( 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} ) ) ) )
( 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) ) )
;
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;
(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
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 ;
( x in H1() & B c= H1() & S2[B] implies S2[B \/ {x}] )
assume I1:
(
x in H1() &
B c= H1() &
S2[
B] )
;
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) }
XBOOLE_0:def 10 { y where y is Element of RR : x in Class ( the InternalRel of RR,y) } c= H . {x}
let w be
object ;
TARSKI:def 3 ( 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) }
;
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;
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) }
XBOOLE_0:def 10 { 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 }
let w be
object ;
TARSKI:def 3 ( 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) }
;
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;
verum
end;
for
X being
Subset of
RR st
X c= B \/ {x} holds
(UAp RR) . X = H . X
hence
S2[
B \/ {x}]
;
verum
end;
S2[ the
carrier of
RR]
from FINSET_1:sch 2(U1, U2, U3);
hence
(UAp RR) . X = H . X
;
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;
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} ) ) )
; ( 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; verum