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 Lm19;
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 Lm20;
the InternalRel of RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #) is_antisymmetric_in the carrier of RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #) by Lm21;
hence RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #) is non empty strict Poset by A1, A2, ORDERS_2:def 2, ORDERS_2:def 3, ORDERS_2:def 4; :: thesis: verum