let P, Q be non empty strict chain-complete Poset; :: thesis: ConRelat P,Q is_reflexive_in ConFuncs P,Q
set R = ConRelat P,Q;
for x being set st x in ConFuncs P,Q holds
[x,x] in ConRelat P,Q

proof

let x be set ; :: thesis: ( x in ConFuncs P,Q implies [x,x] in ConRelat P,Q )
assume B1: x in ConFuncs P,Q ; :: thesis: [x,x] in ConRelat P,Q
then consider x1 being Element of Funcs the carrier of P,the carrier of Q such that
B3: x = x1 and
B4: ex f being continuous Function of P,Q st f = x1 ;
consider f being continuous Function of P,Q such that
B5: f = x1 by B4;
f <= f by Lemlessthan01;
hence [x,x] in ConRelat P,Q by B1, B3, B5, DefConRelat; :: thesis: verum

end;

hence ConRelat P,Q is_reflexive_in ConFuncs P,Q by RELAT_2:def 1; :: thesis: verum