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 )

defpred S₁[ set ] means ( not $1 is empty implies ex_inf_of $1,L );
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
A2: 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
A3: x in X and
Y c= X and
A4: ( not Y is empty implies ex_inf_of Y,L ) ; :: thesis: S₁[Y \/ {x}]
reconsider z = x as Element of L by A3;
assume not Y \/ {x} is empty ; :: thesis: ex_inf_of Y \/ {x},L

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 A5: 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 ) )
A6: Y is_>=_than "/\" (Y,L) by A4, Def10;
A7: ex_inf_of {("/\" (Y,L)),z},L by A1, Th21;
then z >= a by Th19;
then A8: {x} is_>=_than a by Th7;
"/\" (Y,L) >= a by A7, Th19;
then A9: Y is_>=_than a by A6, Th12;
hence Y \/ {x} is_>=_than a by A8, 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} by XBOOLE_1:7;
then Y is_>=_than b by A10;
then A11: "/\" (Y,L) >= b by A4, A5, Def10;
z in {x} by TARSKI:def 1;
then z in Y \/ {x} by XBOOLE_0:def 3;
then z >= b by A10;
hence b <= a by A7, A11, 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
A12: Y \/ {x} is_>=_than c and
A13: for b being Element of L st Y \/ {x} is_>=_than b holds
b <= c ; :: thesis: c = a
Y c= Y \/ {x} by XBOOLE_1:7;
then Y is_>=_than c by A12;
then A14: "/\" (Y,L) >= c by A4, A5, Def10;
z in {x} by TARSKI:def 1;
then z in Y \/ {x} by XBOOLE_0:def 3;
then z >= c by A12;
then A15: c <= a by A7, A14, Th19;
a <= c by A9, A8, A13, Th10;
hence c = a by A15, ORDERS_2:2; :: thesis: verum

end;

end;

end;

end;

A16: S₁[ {} ] ;
A17: X is finite ;
S₁[X] from FINSET_1:sch 2(A17, A16, A2);
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