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