take EnsCat {{}} ; :: thesis: ( EnsCat {{}} is transitive & EnsCat {{}} is associative & EnsCat {{}} is with_units & EnsCat {{}} is strict )
thus ( EnsCat {{}} is transitive & EnsCat {{}} is associative & EnsCat {{}} is with_units & EnsCat {{}} is strict ) by Lm1; :: thesis: verum