let L be non empty Poset; :: thesis: for D being non empty finite filtered Subset of L st ex_inf_of D,L holds
inf D in D
let D be non empty finite filtered Subset of L; :: thesis: ( ex_inf_of D,L implies inf D in D )
assume A1: ex_inf_of D,L ; :: thesis: inf D in D
D c= D ;
then consider d being Element of L such that
A2: ( d in D & d is_<=_than D ) by WAYBEL_0:2;
inf D is_<=_than D by A1, YELLOW_0:31;
then ( inf D <= d & inf D >= d ) by A1, A2, LATTICE3:def 8, YELLOW_0:31;
hence inf D in D by A2, ORDERS_2:25; :: thesis: verum