let P, Q be non empty strict chain-complete Poset; ConRelat (P,Q) is_reflexive_in ConFuncs (P,Q)
set R = ConRelat (P,Q);
for x being object st x in ConFuncs (P,Q) holds
[x,x] in ConRelat (P,Q)
proof
let x be
object ;
( x in ConFuncs (P,Q) implies [x,x] in ConRelat (P,Q) )
assume A1:
x in ConFuncs (
P,
Q)
;
[x,x] in ConRelat (P,Q)
then consider x1 being
Element of
Funcs ( the
carrier of
P, the
carrier of
Q)
such that A2:
x = x1
and A3:
ex
f being
continuous Function of
P,
Q st
f = x1
;
consider f being
continuous Function of
P,
Q such that A4:
f = x1
by A3;
f <= f
by Lm10;
hence
[x,x] in ConRelat (
P,
Q)
by A1, A2, A4, Def7;
verum
end;
hence
ConRelat (P,Q) is_reflexive_in ConFuncs (P,Q)
by RELAT_2:def 1; verum