let L be with_infima Poset; :: thesis: for a, b being Element of L holds inf {a,b} = a "/\" b
let a, b be Element of L; :: thesis: inf {a,b} = a "/\" b
( a "/\" b <= a & a "/\" b <= b ) by Th23;
then A1: a "/\" b is_<=_than {a,b} by Th8;

A2: now

let c be Element of L; :: thesis: ( c is_<=_than {a,b} implies c <= a "/\" b )
assume c is_<=_than {a,b} ; :: thesis: c <= a "/\" b
then ( c <= a & c <= b ) by Th8;
hence c <= a "/\" b by Th23; :: thesis: verum

end;

then ex_inf_of {a,b},L by A1, Th16;
hence inf {a,b} = a "/\" b by A1, A2, Def10; :: thesis: verum