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

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 S_{1}[ 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

A2: "\/" ( { (sup X) where X is non empty directed Subset of L : S_{1}[X] } ,L) = "\/" ((union { X where X is non empty directed Subset of L : S_{1}[X] } ),L)
by Th10;

A3: F = { (sup ({z} "/\" D2)) where z is Element of L : z in D1 }

.= "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S_{1}[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;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 S

( $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

then reconsider F = { (x "/\" y) where x, y is Element of L : ( x in D1 & y in {(sup D2)} ) } as Subset of L ;
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;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

A2: "\/" ( { (sup X) where X is non empty directed Subset of L : S

A3: F = { (sup ({z} "/\" D2)) where z is Element of L : z in D1 }

proof

thus sup ((inf_op L) .: D) =
sup (D1 "/\" D2)
by Th33
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

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;proof

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 )
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;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

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

.= "\/" ( { ("\/" (X,L)) where X is non empty directed Subset of L : S

.= "\/" ( { (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