set A = {} T;
take {} T ; :: thesis: ( {} T is condensed & {} T is subcondensed & {} T is supercondensed )
( {} T is supercondensed & {} T is subcondensed ) by Th4;
hence ( {} T is condensed & {} T is subcondensed & {} T is supercondensed ) ; :: thesis: verum