let P, Q be non empty strict chain-complete Poset; :: thesis: field (ConRelat P,Q) c= ConFuncs P,Q
(ConFuncs P,Q) \/ (ConFuncs P,Q) c= ConFuncs P,Q ;
hence field (ConRelat P,Q) c= ConFuncs P,Q by RELSET_1:19; :: thesis: verum