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:8; :: thesis: verum