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 object st x in field R holds
[x,x] in R

proof

let x be object ; :: thesis: ( x in field R implies [x,x] in R )
assume A1: x in field R ; :: thesis: [x,x] in R
A2: field R c= ConFuncs (P,Q) by Lm13;
R is_reflexive_in ConFuncs (P,Q) by Lm14;
hence [x,x] in R by A1, A2, 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