consider x being Element of L;
take {x} ; :: thesis: ( {x} is directed & {x} is filtered & not {x} is empty & {x} is finite )
thus ( {x} is directed & {x} is filtered & not {x} is empty & {x} is finite ) by Th5; :: thesis: verum