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