let L be non empty Poset; :: thesis: ( L is with_infima iff for X being non empty finite Subset of L holds ex_inf_of X,L )

hereby :: thesis: ( ( for X being non empty finite Subset of L holds ex_inf_of X,L ) implies L is with_infima )

assume A1: L is with_infima ; :: thesis: for X being non empty finite Subset of L holds ex_inf_of X,L
let X be non empty finite Subset of L; :: thesis: ex_inf_of X,L
defpred S₁[ set ] means ( not $1 is empty implies ex_inf_of $1,L );
A2: X is finite ;
A3: S₁[ {} ] ;
A4: for x, Y being set st x in X & Y c= X & S₁[Y] holds
S₁[Y \/ {x}]

proof

let x, Y be set ; :: thesis: ( x in X & Y c= X & S₁[Y] implies S₁[Y \/ {x}] )
assume that
A5: ( x in X & Y c= X ) and
A6: ( not Y is empty implies ex_inf_of Y,L ) ; :: thesis: S₁[Y \/ {x}]
assume not Y \/ {x} is empty ; :: thesis: ex_inf_of Y \/ {x},L
reconsider z = x as Element of L by A5;

per cases ( Y is empty or not Y is empty ) ;

suppose Y is empty ; :: thesis: ex_inf_of Y \/ {x},L

then Y \/ {x} = {z} ;
hence ex_inf_of Y \/ {x},L by Th38; :: thesis: verum

end;

suppose A7: not Y is empty ; :: thesis: ex_inf_of Y \/ {x},L

thus ex_inf_of Y \/ {x},L :: thesis: verum

proof

take a = ("/\" Y,L) "/\" z; :: according to YELLOW_0:def 8 :: thesis: ( Y \/ {x} is_>=_than a & ( for b being Element of L st Y \/ {x} is_>=_than b holds
b <= a ) & ( for c being Element of L st Y \/ {x} is_>=_than c & ( for b being Element of L st Y \/ {x} is_>=_than b holds
b <= c ) holds
c = a ) )
A8: ex_inf_of {("/\" Y,L),z},L by A1, Th21;
then ( Y is_>=_than "/\" Y,L & "/\" Y,L >= a & z >= a ) by A6, A7, Def10, Th19;
then ( Y is_>=_than a & {x} is_>=_than a ) by Th7, Th12;
hence A9: Y \/ {x} is_>=_than a by Th10; :: thesis: ( ( for b being Element of L st Y \/ {x} is_>=_than b holds
b <= a ) & ( for c being Element of L st Y \/ {x} is_>=_than c & ( for b being Element of L st Y \/ {x} is_>=_than b holds
b <= c ) holds
c = a ) )

hereby :: thesis: for c being Element of L st Y \/ {x} is_>=_than c & ( for b being Element of L st Y \/ {x} is_>=_than b holds
b <= c ) holds
c = a

let b be Element of L; :: thesis: ( Y \/ {x} is_>=_than b implies b <= a )
assume A10: Y \/ {x} is_>=_than b ; :: thesis: b <= a
( Y c= Y \/ {x} & z in {x} ) by TARSKI:def 1, XBOOLE_1:7;
then ( Y is_>=_than b & z in Y \/ {x} ) by A10, Th9, XBOOLE_0:def 3;
then ( "/\" Y,L >= b & z >= b ) by A6, A7, A10, Def10, LATTICE3:def 8;
hence b <= a by A8, Th19; :: thesis: verum

end;

let c be Element of L; :: thesis: ( Y \/ {x} is_>=_than c & ( for b being Element of L st Y \/ {x} is_>=_than b holds
b <= c ) implies c = a )
assume that
A11: Y \/ {x} is_>=_than c and
A12: for b being Element of L st Y \/ {x} is_>=_than b holds
b <= c ; :: thesis: c = a
A13: a <= c by A9, A12;
( Y c= Y \/ {x} & z in {x} ) by TARSKI:def 1, XBOOLE_1:7;
then ( Y is_>=_than c & z in Y \/ {x} ) by A11, Th9, XBOOLE_0:def 3;
then ( "/\" Y,L >= c & z >= c ) by A6, A7, A11, Def10, LATTICE3:def 8;
then c <= a by A8, Th19;
hence c = a by A13, ORDERS_2:25; :: thesis: verum

end;

end;

end;

end;

S₁[X] from FINSET_1:sch 2(A2, A3, A4);
hence ex_inf_of X,L ; :: thesis: verum

end;

assume for X being non empty finite Subset of L holds ex_inf_of X,L ; :: thesis: L is with_infima
then for a, b being Element of L holds ex_inf_of {a,b},L ;
hence L is with_infima by Th21; :: thesis: verum