take OrdC 0 ; :: thesis: ( OrdC 0 is strict & OrdC 0 is empty & OrdC 0 is initial )
thus ( OrdC 0 is strict & OrdC 0 is empty & OrdC 0 is initial ) ; :: thesis: verum