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