let S be with_infima Poset; :: thesis: for a, b being Element of S st a <= b holds
lim_inf (Net-Str a,b) = a
let a, b be Element of S; :: thesis: ( a <= b implies lim_inf (Net-Str a,b) = a )
assume A1: a <= b ; :: thesis: lim_inf (Net-Str a,b) = a
reconsider a' = a, b' = b as Element of S ;
lim_inf (Net-Str a,b) = a' "/\" b' by Th7
.= a' by A1, YELLOW_0:25 ;
hence lim_inf (Net-Str a,b) = a ; :: thesis: verum