let H be distributive complete LATTICE; :: thesis: for a being Element of H
for X being finite Subset of H holds inf ({a} "\/" X) = a "\/" (inf X)
let a be Element of H; :: thesis: for X being finite Subset of H holds inf ({a} "\/" X) = a "\/" (inf X)
let X be finite Subset of H; :: thesis: inf ({a} "\/" X) = a "\/" (inf X)
defpred S₁[ set ] means ex A being Subset of H st
( A = $1 & a "\/" (inf A) = inf ({a} "\/" A) );
A1: S₁[ {} ]

proof

reconsider A = {} as Subset of H by XBOOLE_1:2;
take A ; :: thesis: ( A = {} & a "\/" (inf A) = inf ({a} "\/" A) )
thus A = {} ; :: thesis: a "\/" (inf A) = inf ({a} "\/" A)
( a <= Top H & {a} "\/" ({} H) = {} ) by YELLOW_0:45, YELLOW_4:9;
hence a "\/" (inf A) = inf ({a} "\/" A) by YELLOW_0:24; :: thesis: verum

end;

A2: for x, B being set st x in X & B c= X & S₁[B] holds
S₁[B \/ {x}]

proof

let x, B be set ; :: thesis: ( x in X & B c= X & S₁[B] implies S₁[B \/ {x}] )
assume that
A3: x in X and
A4: B c= X and
A5: S₁[B] ; :: thesis: S₁[B \/ {x}]
reconsider x1 = x as Element of H by A3;
A6: {x1} c= the carrier of H ;
B c= the carrier of H by A4, XBOOLE_1:1;
then reconsider C = B \/ {x} as Subset of H by A6, XBOOLE_1:8;
take C ; :: thesis: ( C = B \/ {x} & a "\/" (inf C) = inf ({a} "\/" C) )
thus C = B \/ {x} ; :: thesis: a "\/" (inf C) = inf ({a} "\/" C)
consider A being Subset of H such that
A7: A = B and
A8: a "\/" (inf A) = inf ({a} "\/" A) by A5;
A9: {a} "\/" C = ({a} "\/" A) \/ ({a} "\/" {x1}) by A7, YELLOW_4:16
.= ({a} "\/" A) \/ {(a "\/" x1)} by YELLOW_4:19 ;
A10: ( ex_inf_of {a} "\/" A,H & ex_inf_of {(a "\/" x1)},H ) by YELLOW_0:17;
( ex_inf_of B,H & ex_inf_of {x},H ) by YELLOW_0:17;
hence a "\/" (inf C) = a "\/" (("/\" (B,H)) "/\" ("/\" ({x},H))) by YELLOW_2:4
.= (inf ({a} "\/" A)) "/\" (a "\/" ("/\" ({x},H))) by A7, A8, WAYBEL_1:5
.= (inf ({a} "\/" A)) "/\" (a "\/" x1) by YELLOW_0:39
.= (inf ({a} "\/" A)) "/\" (inf {(a "\/" x1)}) by YELLOW_0:39
.= inf ({a} "\/" C) by A10, A9, YELLOW_2:4 ;
:: thesis: verum

end;

A11: X is finite ;
S₁[X] from FINSET_1:sch 2(A11, A1, A2);
hence inf ({a} "\/" X) = a "\/" (inf X) ; :: thesis: verum