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

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