ConRelat (P,Q) is_reflexive_in field (ConRelat (P,Q))

proof

reconsider R = ConRelat (P,Q) as Relation of (ConFuncs (P,Q)) ;
for x being set st x in field R holds
[x,x] in R

proof

let x be set ; :: thesis: ( x in field R implies [x,x] in R )
assume B0: x in field R ; :: thesis: [x,x] in R
B1: field R c= ConFuncs (P,Q) by LemConRelat01;
R is_reflexive_in ConFuncs (P,Q) by LemConRelat02;
hence [x,x] in R by B0, B1, RELAT_2:def 1; :: thesis: verum

end;

hence ConRelat (P,Q) is_reflexive_in field (ConRelat (P,Q)) by RELAT_2:def 1; :: thesis: verum

end;

hence ConRelat (P,Q) is reflexive by RELAT_2:def 9; :: thesis: verum