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

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