set R = the non empty transitive directed RelStr ;
set p = the Element of T;
take ConstantNet ( the non empty transitive directed RelStr , the Element of T) ; :: thesis: ( ConstantNet ( the non empty transitive directed RelStr , the Element of T) is constant & ConstantNet ( the non empty transitive directed RelStr , the Element of T) is strict )
thus ( ConstantNet ( the non empty transitive directed RelStr , the Element of T) is constant & ConstantNet ( the non empty transitive directed RelStr , the Element of T) is strict ) ; :: thesis: verum