defpred S₁[ set ] means $1 is tagged_division of A;
consider R being set such that
A1: for x being set holds
( x in R iff ( x in [:(bool [:NAT,REAL:]),(REAL *):] & S₁[x] ) ) from XFAMILY:sch 1();
take R ; :: thesis: for x being set holds
( x in R iff x is tagged_division of A )
let x be set ; :: thesis: ( x in R iff x is tagged_division of A )
thus ( x in R implies x is tagged_division of A ) by A1; :: thesis: ( x is tagged_division of A implies x in R )
assume x is tagged_division of A ; :: thesis: x in R
then reconsider p = x as tagged_division of A ;
consider D being Division of A, T being Element of set_of_tagged_Division D such that
A2: p = [D,T] by COUSIN:def 3;
[D,T] in [:(bool [:NAT,REAL:]),(REAL *):] by ZFMISC_1:87;
hence x in R by A1, A2; :: thesis: verum