let P, Q be non empty strict chain-complete Poset; :: thesis: ConRelat (P,Q) is_antisymmetric_in ConFuncs (P,Q)
set X = ConFuncs (P,Q);
reconsider R = ConRelat (P,Q) as Relation of (ConFuncs (P,Q)) ;
for x, y being object st x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & [x,y] in R & [y,x] in R holds
x = y

proof

let x, y be object ; :: thesis: ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & [x,y] in R & [y,x] in R implies x = y )
assume A1: ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & [x,y] in R & [y,x] in R ) ; :: thesis: x = y
then consider f, g being Function of P,Q such that
A2: ( x = f & y = g & f <= g ) by Def7;
consider g1, f1 being Function of P,Q such that
A3: ( y = g1 & x = f1 & g1 <= f1 ) by A1, Def7;
thus x = y by A2, A3, Lm12; :: thesis: verum

end;

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