take EnsCat NAT ; :: thesis: ( EnsCat NAT is concrete & EnsCat NAT is quasi-functional & EnsCat NAT is strict )
thus ( EnsCat NAT is concrete & EnsCat NAT is quasi-functional & EnsCat NAT is strict ) ; :: thesis: verum