consider D being Division of I, T being Element of set_of_tagged_Division D such that
A1: TD = [D,T] by Def3;
take D ; :: thesis: ex D being Division of I ex T being Element of set_of_tagged_Division D st
( D = D & TD = [D,T] )
thus ex D being Division of I ex T being Element of set_of_tagged_Division D st
( D = D & TD = [D,T] ) by A1; :: thesis: verum