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