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 set 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 set ; :: thesis: ( x in ConFuncs P,Q & y in ConFuncs P,Q & [x,y] in R & [y,x] in R implies x = y )
assume B1: ( 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
B2: ( x = f & y = g & f <= g ) by DefConRelat;
consider g1, f1 being Function of P,Q such that
B3: ( y = g1 & x = f1 & g1 <= f1 ) by B1, DefConRelat;
thus x = y by B2, B3, Lemlessthan03; :: thesis: verum

end;

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