let L be Semilattice; :: thesis: for D being non empty directed Subset of [:L,L:] holds union { X where X is non empty directed Subset of L : ex x being Element of L st

( X = {x} "/\" (proj2 D) & x in proj1 D ) } = (proj1 D) "/\" (proj2 D)

let D be non empty directed Subset of [:L,L:]; :: thesis: union { X where X is non empty directed Subset of L : ex x being Element of L st

( X = {x} "/\" (proj2 D) & x in proj1 D ) } = (proj1 D) "/\" (proj2 D)

set D1 = proj1 D;

set D2 = proj2 D;

defpred S_{1}[ set ] means ex x being Element of L st

( $1 = {x} "/\" (proj2 D) & x in proj1 D );

reconsider T = proj2 D as non empty directed Subset of L by YELLOW_3:21, YELLOW_3:22;

A1: (proj1 D) "/\" (proj2 D) = { (x "/\" y) where x, y is Element of L : ( x in proj1 D & y in proj2 D ) } by YELLOW_4:def 4;

thus union { X where X is non empty directed Subset of L : S_{1}[X] } c= (proj1 D) "/\" (proj2 D)
:: according to XBOOLE_0:def 10 :: thesis: (proj1 D) "/\" (proj2 D) c= union { X where X is non empty directed Subset of L : ex x being Element of L st

( X = {x} "/\" (proj2 D) & x in proj1 D ) }

( X = {x} "/\" (proj2 D) & x in proj1 D ) } )

assume q in (proj1 D) "/\" (proj2 D) ; :: thesis: q in union { X where X is non empty directed Subset of L : ex x being Element of L st

( X = {x} "/\" (proj2 D) & x in proj1 D ) }

then consider x, y being Element of L such that

A8: q = x "/\" y and

A9: x in proj1 D and

A10: y in proj2 D by A1;

reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0:5;

( not xx "/\" T is empty & xx "/\" T is directed ) ;

then A11: {x} "/\" (proj2 D) in { X where X is non empty directed Subset of L : S_{1}[X] }
by A9;

{x} "/\" (proj2 D) = { (x "/\" d) where d is Element of L : d in proj2 D } by YELLOW_4:42;

then q in {x} "/\" (proj2 D) by A8, A10;

hence q in union { X where X is non empty directed Subset of L : ex x being Element of L st

( X = {x} "/\" (proj2 D) & x in proj1 D ) } by A11, TARSKI:def 4; :: thesis: verum

( X = {x} "/\" (proj2 D) & x in proj1 D ) } = (proj1 D) "/\" (proj2 D)

let D be non empty directed Subset of [:L,L:]; :: thesis: union { X where X is non empty directed Subset of L : ex x being Element of L st

( X = {x} "/\" (proj2 D) & x in proj1 D ) } = (proj1 D) "/\" (proj2 D)

set D1 = proj1 D;

set D2 = proj2 D;

defpred S

( $1 = {x} "/\" (proj2 D) & x in proj1 D );

reconsider T = proj2 D as non empty directed Subset of L by YELLOW_3:21, YELLOW_3:22;

A1: (proj1 D) "/\" (proj2 D) = { (x "/\" y) where x, y is Element of L : ( x in proj1 D & y in proj2 D ) } by YELLOW_4:def 4;

thus union { X where X is non empty directed Subset of L : S

( X = {x} "/\" (proj2 D) & x in proj1 D ) }

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in (proj1 D) "/\" (proj2 D) or q in union { X where X is non empty directed Subset of L : ex x being Element of L st
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in union { X where X is non empty directed Subset of L : S_{1}[X] } or q in (proj1 D) "/\" (proj2 D) )

assume q in union { X where X is non empty directed Subset of L : S_{1}[X] }
; :: thesis: q in (proj1 D) "/\" (proj2 D)

then consider w being set such that

A2: q in w and

A3: w in { X where X is non empty directed Subset of L : S_{1}[X] }
by TARSKI:def 4;

consider e being non empty directed Subset of L such that

A4: w = e and

A5: S_{1}[e]
by A3;

consider p being Element of L such that

A6: e = {p} "/\" (proj2 D) and

A7: p in proj1 D by A5;

{p} "/\" (proj2 D) = { (p "/\" y) where y is Element of L : y in proj2 D } by YELLOW_4:42;

then ex y being Element of L st

( q = p "/\" y & y in proj2 D ) by A2, A4, A6;

hence q in (proj1 D) "/\" (proj2 D) by A1, A7; :: thesis: verum

end;assume q in union { X where X is non empty directed Subset of L : S

then consider w being set such that

A2: q in w and

A3: w in { X where X is non empty directed Subset of L : S

consider e being non empty directed Subset of L such that

A4: w = e and

A5: S

consider p being Element of L such that

A6: e = {p} "/\" (proj2 D) and

A7: p in proj1 D by A5;

{p} "/\" (proj2 D) = { (p "/\" y) where y is Element of L : y in proj2 D } by YELLOW_4:42;

then ex y being Element of L st

( q = p "/\" y & y in proj2 D ) by A2, A4, A6;

hence q in (proj1 D) "/\" (proj2 D) by A1, A7; :: thesis: verum

( X = {x} "/\" (proj2 D) & x in proj1 D ) } )

assume q in (proj1 D) "/\" (proj2 D) ; :: thesis: q in union { X where X is non empty directed Subset of L : ex x being Element of L st

( X = {x} "/\" (proj2 D) & x in proj1 D ) }

then consider x, y being Element of L such that

A8: q = x "/\" y and

A9: x in proj1 D and

A10: y in proj2 D by A1;

reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0:5;

( not xx "/\" T is empty & xx "/\" T is directed ) ;

then A11: {x} "/\" (proj2 D) in { X where X is non empty directed Subset of L : S

{x} "/\" (proj2 D) = { (x "/\" d) where d is Element of L : d in proj2 D } by YELLOW_4:42;

then q in {x} "/\" (proj2 D) by A8, A10;

hence q in union { X where X is non empty directed Subset of L : ex x being Element of L st

( X = {x} "/\" (proj2 D) & x in proj1 D ) } by A11, TARSKI:def 4; :: thesis: verum