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

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