take OrdC 1 ; :: thesis: ( OrdC 1 is strict & not OrdC 1 is empty & OrdC 1 is terminal )
thus ( OrdC 1 is strict & not OrdC 1 is empty & OrdC 1 is terminal ) ; :: thesis: verum