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

A1: now :: thesis: for c being Element of L st c is_<=_than {a,b} holds
c <= a "/\" b

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;

( a "/\" b <= a & a "/\" b <= b ) by Th23;
then A2: a "/\" b is_<=_than {a,b} by Th8;
then ex_inf_of {a,b},L by A1, Th16;
hence inf {a,b} = a "/\" b by A2, A1, Def10; :: thesis: verum