for ET being FMT_TopSpace
for B being Basis of ET holds
( ( for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB ) & the carrier of ET = union B )