consider x being Element of T;
take {x} ; :: thesis: ( not {x} is empty & {x} is directed & {x} is finite )
thus ( not {x} is empty & {x} is directed & {x} is finite ) by WAYBEL_0:5; :: thesis: verum