let T be InsType of (Trivial-AMI IL,N); :: according to AMISTD_2:def 11 :: thesis: AddressParts T is product-like
take {} ; :: according to CARD_3:def 14 :: thesis: AddressParts T = product {}
thus AddressParts T = product {} by Lm4, CARD_3:19; :: thesis: verum