for L being non empty Poset
for x being Element of L holds
( ex_inf_of uparrow x,L & inf (uparrow x) = x )