let f be object ; :: according to FUNCT_1:def 13 :: thesis: ( not f in AddressParts T or f is set )
assume f in AddressParts T ; :: thesis: f is set
then ex I being Element of S st
( f = AddressPart I & InsCode I = T ) ;
hence f is set ; :: thesis: verum