let L be with_infima Poset; :: thesis: for X being Subset of L st ( ex_inf_of X,L or L is complete ) holds

inf X = inf (fininfs X)

let X be Subset of L; :: thesis: ( ( ex_inf_of X,L or L is complete ) implies inf X = inf (fininfs X) )

assume ( ex_inf_of X,L or L is complete ) ; :: thesis: inf X = inf (fininfs X)

then A1: ex_inf_of X,L by YELLOW_0:17;

inf X = inf (fininfs X)

let X be Subset of L; :: thesis: ( ( ex_inf_of X,L or L is complete ) implies inf X = inf (fininfs X) )

assume ( ex_inf_of X,L or L is complete ) ; :: thesis: inf X = inf (fininfs X)

then A1: ex_inf_of X,L by YELLOW_0:17;

A2: now :: thesis: for Y being finite Subset of X st Y <> {} holds

ex_inf_of Y,L

ex_inf_of Y,L

let Y be finite Subset of X; :: thesis: ( Y <> {} implies ex_inf_of Y,L )

Y c= the carrier of L by XBOOLE_1:1;

hence ( Y <> {} implies ex_inf_of Y,L ) by YELLOW_0:55; :: thesis: verum

end;Y c= the carrier of L by XBOOLE_1:1;

hence ( Y <> {} implies ex_inf_of Y,L ) by YELLOW_0:55; :: thesis: verum

A3: now :: thesis: for x being Element of L st x in fininfs X holds

ex Y being finite Subset of X st

( ex_inf_of Y,L & x = "/\" (Y,L) )

ex Y being finite Subset of X st

( ex_inf_of Y,L & x = "/\" (Y,L) )

let x be Element of L; :: thesis: ( x in fininfs X implies ex Y being finite Subset of X st

( ex_inf_of Y,L & x = "/\" (Y,L) ) )

assume x in fininfs X ; :: thesis: ex Y being finite Subset of X st

( ex_inf_of Y,L & x = "/\" (Y,L) )

then ex Y being finite Subset of X st

( x = "/\" (Y,L) & ex_inf_of Y,L ) ;

hence ex Y being finite Subset of X st

( ex_inf_of Y,L & x = "/\" (Y,L) ) ; :: thesis: verum

end;( ex_inf_of Y,L & x = "/\" (Y,L) ) )

assume x in fininfs X ; :: thesis: ex Y being finite Subset of X st

( ex_inf_of Y,L & x = "/\" (Y,L) )

then ex Y being finite Subset of X st

( x = "/\" (Y,L) & ex_inf_of Y,L ) ;

hence ex Y being finite Subset of X st

( ex_inf_of Y,L & x = "/\" (Y,L) ) ; :: thesis: verum

now :: thesis: for Y being finite Subset of X st Y <> {} holds

"/\" (Y,L) in fininfs X

hence
inf X = inf (fininfs X)
by A1, A2, A3, Th59; :: thesis: verum"/\" (Y,L) in fininfs X

let Y be finite Subset of X; :: thesis: ( Y <> {} implies "/\" (Y,L) in fininfs X )

reconsider Z = Y as Subset of L by XBOOLE_1:1;

assume Y <> {} ; :: thesis: "/\" (Y,L) in fininfs X

then ex_inf_of Z,L by YELLOW_0:55;

hence "/\" (Y,L) in fininfs X ; :: thesis: verum

end;reconsider Z = Y as Subset of L by XBOOLE_1:1;

assume Y <> {} ; :: thesis: "/\" (Y,L) in fininfs X

then ex_inf_of Z,L by YELLOW_0:55;

hence "/\" (Y,L) in fininfs X ; :: thesis: verum