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