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 a9 = a, b9 = b as Element of S ;
lim_inf (Net-Str (a,b)) = a9 "/\" b9 by Th7
.= a9 by A1, YELLOW_0:25 ;
hence lim_inf (Net-Str (a,b)) = a ; :: thesis: verum