set C = the empty strict CategoryStr ;
take the empty strict CategoryStr ; :: thesis: ( the empty strict CategoryStr is strict & the empty strict CategoryStr is preorder )
thus ( the empty strict CategoryStr is strict & the empty strict CategoryStr is preorder ) ; :: thesis: verum