let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being AMI-Struct of IL,N
for p being PartState of S holds dom p c= the carrier of S
let N be with_non-empty_elements set ; :: thesis: for S being AMI-Struct of IL,N
for p being PartState of S holds dom p c= the carrier of S
let S be AMI-Struct of IL,N; :: thesis: for p being PartState of S holds dom p c= the carrier of S
let p be PartState of S; :: thesis: dom p c= the carrier of S
dom p c= dom the Object-Kind of S by CARD_3:65;
hence dom p c= the carrier of S by FUNCT_2:def 1; :: thesis: verum