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

proof

reconsider A = {} as Subset of H by XBOOLE_1:2;
take A ; :: thesis: ( A = {} & a "/\" (sup A) = sup ({a} "/\" A) )
thus A = {} ; :: thesis: a "/\" (sup A) = sup ({a} "/\" A)
A3: Bottom H <= a by YELLOW_0:44;
{a} "/\" ({} H) = {} by YELLOW_4:36;
hence a "/\" (sup A) = sup ({a} "/\" A) by A3, YELLOW_0:25; :: thesis: verum

end;

A4: 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
A5: ( x in X & B c= X ) and
A6: S₁[B] ; :: thesis: S₁[B \/ {x}]
consider A being Subset of H such that
A7: ( A = B & a "/\" (sup A) = sup ({a} "/\" A) ) by A6;
reconsider x1 = x as Element of H by A5;
( B c= the carrier of H & {x1} c= the carrier of H ) by A5, XBOOLE_1:1;
then reconsider C = B \/ {x} as Subset of H by XBOOLE_1:8;
take C ; :: thesis: ( C = B \/ {x} & a "/\" (sup C) = sup ({a} "/\" C) )
thus C = B \/ {x} ; :: thesis: a "/\" (sup C) = sup ({a} "/\" C)
A8: ( ex_sup_of {a} "/\" A,H & ex_sup_of {(a "/\" x1)},H ) by YELLOW_0:17;
A9: {a} "/\" C = ({a} "/\" A) \/ ({a} "/\" {x1}) by A7, YELLOW_4:43
.= ({a} "/\" A) \/ {(a "/\" x1)} by YELLOW_4:46 ;
( ex_sup_of B,H & ex_sup_of {x},H ) by YELLOW_0:17;
hence a "/\" (sup C) = a "/\" (("\/" B,H) "\/" ("\/" {x},H)) by YELLOW_2:3
.= (sup ({a} "/\" A)) "\/" (a "/\" ("\/" {x},H)) by A7, WAYBEL_1:def 3
.= (sup ({a} "/\" A)) "\/" (a "/\" x1) by YELLOW_0:39
.= (sup ({a} "/\" A)) "\/" (sup {(a "/\" x1)}) by YELLOW_0:39
.= sup ({a} "/\" C) by A8, A9, YELLOW_2:3 ;
:: thesis: verum

end;

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