let L be up-complete Semilattice; ( ( for x being Element of L
for E being non empty directed Subset of L st x <= sup E holds
x <= sup ({x} "/\" E) ) implies inf_op L is directed-sups-preserving )
assume A1:
for x being Element of L
for E being non empty directed Subset of L st x <= sup E holds
x <= sup ({x} "/\" E)
; inf_op L is directed-sups-preserving
let D be Subset of [:L,L:]; WAYBEL_0:def 37 ( D is empty or not D is directed or inf_op L preserves_sup_of D )
assume
( not D is empty & D is directed )
; inf_op L preserves_sup_of D
then reconsider DD = D as non empty directed Subset of [:L,L:] ;
thus
inf_op L preserves_sup_of D
verumproof
reconsider D1 =
proj1 DD,
D2 =
proj2 DD as non
empty directed Subset of
L by YELLOW_3:21, YELLOW_3:22;
reconsider C = the
carrier of
L as non
empty set ;
set f =
inf_op L;
assume
ex_sup_of D,
[:L,L:]
;
WAYBEL_0:def 31 ( ex_sup_of (inf_op L) .: D,L & "\/" (((inf_op L) .: D),L) = (inf_op L) . ("\/" (D,[:L,L:])) )
set d2 =
sup D2;
defpred S1[
set ]
means ex
x being
Element of
L st
( $1
= {x} "/\" D2 &
x in D1 );
(inf_op L) .: DD is
directed
by YELLOW_2:15;
hence
ex_sup_of (inf_op L) .: D,
L
by WAYBEL_0:75;
"\/" (((inf_op L) .: D),L) = (inf_op L) . ("\/" (D,[:L,L:]))
{ (x "/\" y) where x, y is Element of L : ( x in D1 & y in {(sup D2)} ) } c= C
then reconsider F =
{ (x "/\" y) where x, y is Element of L : ( x in D1 & y in {(sup D2)} ) } as
Subset of
L ;
A2:
"\/" (
{ (sup X) where X is non empty directed Subset of L : S1[X] } ,
L)
= "\/" (
(union { X where X is non empty directed Subset of L : S1[X] } ),
L)
by Th10;
A3:
F = { (sup ({z} "/\" D2)) where z is Element of L : z in D1 }
thus sup ((inf_op L) .: D) =
sup (D1 "/\" D2)
by Th33
.=
"\/" (
{ ("\/" (X,L)) where X is non empty directed Subset of L : S1[X] } ,
L)
by A2, Th6
.=
"\/" (
{ (sup ({x} "/\" D2)) where x is Element of L : x in D1 } ,
L)
by Th5
.=
sup ({(sup D2)} "/\" D1)
by A3, YELLOW_4:def 4
.=
(sup D1) "/\" (sup D2)
by A1, Th28
.=
(inf_op L) . (
(sup D1),
(sup D2))
by Def4
.=
(inf_op L) . (sup D)
by Th12
;
verum
end;