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 and
A3: d is_<=_than D by WAYBEL_0:2;
A4: inf D >= d by A1, A3, YELLOW_0:31;
inf D is_<=_than D by A1, YELLOW_0:31;
then inf D <= d by A2;
hence inf D in D by A2, A4, ORDERS_2:2; :: thesis: verum