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_{1}[ set ] means ex A being Subset of H st

( A = $1 & a "/\" (sup A) = sup ({a} "/\" A) );

A1: S_{1}[ {} ]
_{1}[B] holds

S_{1}[B \/ {x}]

S_{1}[X]
from FINSET_1:sch 2(A11, A1, A2);

hence sup ({a} "/\" X) = a "/\" (sup X) ; :: thesis: verum

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

( A = $1 & a "/\" (sup A) = sup ({a} "/\" A) );

A1: S

proof

A2:
for x, B being set st x in X & B c= X & S
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)

( Bottom H <= a & {a} "/\" ({} H) = {} ) by YELLOW_0:44, YELLOW_4:36;

hence a "/\" (sup A) = sup ({a} "/\" A) by YELLOW_0:25; :: thesis: verum

end;take A ; :: thesis: ( A = {} & a "/\" (sup A) = sup ({a} "/\" A) )

thus A = {} ; :: thesis: a "/\" (sup A) = sup ({a} "/\" A)

( Bottom H <= a & {a} "/\" ({} H) = {} ) by YELLOW_0:44, YELLOW_4:36;

hence a "/\" (sup A) = sup ({a} "/\" A) by YELLOW_0:25; :: thesis: verum

S

proof

A11:
X is finite
;
let x, B be set ; :: thesis: ( x in X & B c= X & S_{1}[B] implies S_{1}[B \/ {x}] )

assume that

A3: x in X and

A4: B c= X and

A5: S_{1}[B]
; :: thesis: S_{1}[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 "/\" (sup C) = sup ({a} "/\" C) )

thus C = B \/ {x} ; :: thesis: a "/\" (sup C) = sup ({a} "/\" C)

consider A being Subset of H such that

A7: A = B and

A8: a "/\" (sup A) = sup ({a} "/\" A) by A5;

A9: {a} "/\" C = ({a} "/\" A) \/ ({a} "/\" {x1}) by A7, YELLOW_4:43

.= ({a} "/\" A) \/ {(a "/\" x1)} by YELLOW_4:46 ;

A10: ( ex_sup_of {a} "/\" A,H & ex_sup_of {(a "/\" x1)},H ) by YELLOW_0:17;

( 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, A8, 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 A10, A9, YELLOW_2:3 ;

:: thesis: verum

end;assume that

A3: x in X and

A4: B c= X and

A5: S

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 "/\" (sup C) = sup ({a} "/\" C) )

thus C = B \/ {x} ; :: thesis: a "/\" (sup C) = sup ({a} "/\" C)

consider A being Subset of H such that

A7: A = B and

A8: a "/\" (sup A) = sup ({a} "/\" A) by A5;

A9: {a} "/\" C = ({a} "/\" A) \/ ({a} "/\" {x1}) by A7, YELLOW_4:43

.= ({a} "/\" A) \/ {(a "/\" x1)} by YELLOW_4:46 ;

A10: ( ex_sup_of {a} "/\" A,H & ex_sup_of {(a "/\" x1)},H ) by YELLOW_0:17;

( 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, A8, 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 A10, A9, YELLOW_2:3 ;

:: thesis: verum

S

hence sup ({a} "/\" X) = a "/\" (sup X) ; :: thesis: verum