let I be non empty closed_interval Subset of REAL; :: thesis: for TD being tagged_division of I
for D being Division of I
for T being Element of set_of_tagged_Division D st TD = [D,T] holds
( T = tagged_of TD & D = division_of TD )
let TD be tagged_division of I; :: thesis: for D being Division of I
for T being Element of set_of_tagged_Division D st TD = [D,T] holds
( T = tagged_of TD & D = division_of TD )
let D be Division of I; :: thesis: for T being Element of set_of_tagged_Division D st TD = [D,T] holds
( T = tagged_of TD & D = division_of TD )
let T be Element of set_of_tagged_Division D; :: thesis: ( TD = [D,T] implies ( T = tagged_of TD & D = division_of TD ) )
assume A1: TD = [D,T] ; :: thesis: ( T = tagged_of TD & D = division_of TD )
ex D1 being Division of I ex T1 being Element of set_of_tagged_Division D1 st
( tagged_of TD = T1 & TD = [D1,T1] ) by Def2;
hence ( T = tagged_of TD & D = division_of TD ) by A1, XTUPLE_0:1, COUSIN:def 6; :: thesis: verum