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