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 object 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 object ; :: 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 A5: ( 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);
A6: field R c= ConFuncs (P,Q) by Lm13;
R is_antisymmetric_in ConFuncs (P,Q) by Lm16;
hence x = y by A5, A6, 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