set IT = RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #);
A1: the InternalRel of RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #) is_reflexive_in the carrier of RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #) by LemConRelat02;
A2: the InternalRel of RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #) is_transitive_in the carrier of RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #) by LemConRelat03;
the InternalRel of RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #) is_antisymmetric_in the carrier of RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #) by LemConRelat04;
hence RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #) is non empty strict Poset by A1, A2, ORDERS_2:def 4, ORDERS_2:def 5, ORDERS_2:def 6; :: thesis: verum