let A be non empty finite set ; for U being Function of (bool A),(bool A) st U . {} = {} & ( for X being Subset of A holds X c= U . X ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds
ex R being non empty finite reflexive RelStr st
( the carrier of R = A & U = UAp R )
let U be Function of (bool A),(bool A); ( U . {} = {} & ( for X being Subset of A holds X c= U . X ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) implies ex R being non empty finite reflexive RelStr st
( the carrier of R = A & U = UAp R ) )
assume that
A1:
U . {} = {}
and
A2:
for X being Subset of A holds X c= U . X
and
A3:
for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y)
; ex R being non empty finite reflexive RelStr st
( the carrier of R = A & U = UAp R )
( U . ([#] A) c= [#] A & [#] A c= U . ([#] A) )
by A2;
then
U . A = A
;
then consider R being non empty finite serial RelStr such that
A4:
( the carrier of R = A & U = UAp R )
by Th32, A1, A3;
for x being object st x in the carrier of R holds
[x,x] in the InternalRel of R
proof
let x be
object ;
( x in the carrier of R implies [x,x] in the InternalRel of R )
assume A5:
x in the
carrier of
R
;
[x,x] in the InternalRel of R
then A6:
{x} is
Subset of
R
by ZFMISC_1:31;
reconsider Z =
{x} as
Subset of
R by A5, ZFMISC_1:31;
A7:
{x} c= U . {x}
by A4, A6, A2;
x in {x}
by TARSKI:def 1;
then A8:
x in U . {x}
by A7;
U . {x} =
UAp Z
by Def11, A4
.=
{ y where y is Element of R : Class ( the InternalRel of R,y) meets Z }
;
then consider t being
Element of
R such that A9:
(
t = x &
Class ( the
InternalRel of
R,
t)
meets Z )
by A8;
x in Class ( the
InternalRel of
R,
t)
hence
[x,x] in the
InternalRel of
R
by A9, RELAT_1:169;
verum
end;
then
R is reflexive
by ORDERS_2:def 2, RELAT_2:def 1;
hence
ex R being non empty finite reflexive RelStr st
( the carrier of R = A & U = UAp R )
by A4; verum