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