let L be non empty Poset; :: thesis: for x being Element of L holds
( ex_inf_of uparrow x,L & inf (uparrow x) = x )
let x be Element of L; :: thesis: ( ex_inf_of uparrow x,L & inf (uparrow x) = x )
A1: ( uparrow x = uparrow {x} & ex_inf_of {x},L ) by YELLOW_0:38;
hence ex_inf_of uparrow x,L by Th37; :: thesis: inf (uparrow x) = x
thus inf (uparrow x) = inf {x} by A1, Th38
.= x by YELLOW_0:39 ; :: thesis: verum