let L be up-complete Semilattice; :: thesis: ( ( 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) ; :: thesis: inf_op L is directed-sups-preserving
let D be Subset of [:L,L:]; :: according to WAYBEL_0:def 37 :: thesis: ( D is empty or not D is directed or inf_op L preserves_sup_of D )
assume ( not D is empty & D is directed ) ; :: thesis: 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 :: thesis: verum
proof
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:] ; :: according to WAYBEL_0:def 31 :: thesis: ( 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; :: thesis: "\/" (((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
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in { (x "/\" y) where x, y is Element of L : ( x in D1 & y in {(sup D2)} ) } or q in C )
assume q in { (x "/\" y) where x, y is Element of L : ( x in D1 & y in {(sup D2)} ) } ; :: thesis: q in C
then ex x, y being Element of L st
( q = x "/\" y & x in D1 & y in {(sup D2)} ) ;
hence q in C ; :: thesis: verum
end;
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 }
proof
thus F c= { (sup ({z} "/\" D2)) where z is Element of L : z in D1 } :: according to XBOOLE_0:def 10 :: thesis: { (sup ({z} "/\" D2)) where z is Element of L : z in D1 } c= F
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in F or q in { (sup ({z} "/\" D2)) where z is Element of L : z in D1 } )
assume q in F ; :: thesis: q in { (sup ({z} "/\" D2)) where z is Element of L : z in D1 }
then consider x, y being Element of L such that
A4: q = x "/\" y and
A5: x in D1 and
A6: y in {(sup D2)} ;
q = x "/\" (sup D2) by A4, A6, TARSKI:def 1
.= sup ({x} "/\" D2) by A1, Th28 ;
hence q in { (sup ({z} "/\" D2)) where z is Element of L : z in D1 } by A5; :: thesis: verum
end;
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in { (sup ({z} "/\" D2)) where z is Element of L : z in D1 } or q in F )
A7: sup D2 in {(sup D2)} by TARSKI:def 1;
assume q in { (sup ({z} "/\" D2)) where z is Element of L : z in D1 } ; :: thesis: q in F
then consider z being Element of L such that
A8: q = sup ({z} "/\" D2) and
A9: z in D1 ;
q = z "/\" (sup D2) by A1, A8, Th28;
hence q in F by A9, A7; :: thesis: verum
end;
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 ; :: thesis: verum
end;