let H be distributive complete LATTICE; 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; for X being finite Subset of H holds sup ({a} "/\" X) = a "/\" (sup X)
let X be finite Subset of H; sup ({a} "/\" X) = a "/\" (sup X)
defpred S1[ set ] means ex A being Subset of H st
( A = $1 & a "/\" (sup A) = sup ({a} "/\" A) );
A1:
S1[ {} ]
A2:
for x, B being set st x in X & B c= X & S1[B] holds
S1[B \/ {x}]
proof
let x,
B be
set ;
( x in X & B c= X & S1[B] implies S1[B \/ {x}] )
assume that A3:
x in X
and A4:
B c= X
and A5:
S1[
B]
;
S1[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
;
( C = B \/ {x} & a "/\" (sup C) = sup ({a} "/\" C) )
thus
C = B \/ {x}
;
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
;
verum
end;
A11:
X is finite
;
S1[X]
from FINSET_1:sch 2(A11, A1, A2);
hence
sup ({a} "/\" X) = a "/\" (sup X)
; verum