ConRelat (P,Q) is_antisymmetric_in field (ConRelat (P,Q))

proof

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

proof

let x, y be set ; :: thesis: ( x in field (ConRelat (P,Q)) & y in field (ConRelat (P,Q)) & [x,y] in R & [y,x] in R implies x = y )
assume B0: ( x in field (ConRelat (P,Q)) & y in field (ConRelat (P,Q)) & [x,y] in R & [y,x] in R ) ; :: thesis: x = y
set X1 = ConFuncs (P,Q);
B1: field R c= ConFuncs (P,Q) by LemConRelat01;
R is_antisymmetric_in ConFuncs (P,Q) by LemConRelat04;
hence x = y by B0, B1, RELAT_2:def 4; :: thesis: verum

end;

hence ConRelat (P,Q) is_antisymmetric_in field (ConRelat (P,Q)) by RELAT_2:def 4; :: thesis: verum

end;

hence ConRelat (P,Q) is antisymmetric by RELAT_2:def 12; :: thesis: verum