:: YELLOW_3 semantic presentation begin scheme :: YELLOW_3:sch 1 FraenkelA2{ F1() -> non empty set , F2( set , set ) -> set , P1[ set , set ], P2[ set , set ] } : { F2(s,t) where s, t is Element of F1() : P1[s,t] } is Subset of F1() provided A1: for s, t being Element of F1() holds F2(s,t) in F1() proof { F2(s,t) where s, t is Element of F1() : P1[s,t] } c= F1() proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { F2(s,t) where s, t is Element of F1() : P1[s,t] } or q in F1() ) assume q in { F2(s,t) where s, t is Element of F1() : P1[s,t] } ; ::_thesis: q in F1() then ex s, t being Element of F1() st ( q = F2(s,t) & P1[s,t] ) ; hence q in F1() by A1; ::_thesis: verum end; hence { F2(s,t) where s, t is Element of F1() : P1[s,t] } is Subset of F1() ; ::_thesis: verum end; registration let L be RelStr ; let X be empty Subset of L; cluster downarrow X -> empty ; coherence downarrow X is empty proof assume not downarrow X is empty ; ::_thesis: contradiction then consider x being set such that A1: x in downarrow X by XBOOLE_0:def_1; reconsider x = x as Element of L by A1; ex z being Element of L st ( x <= z & z in X ) by A1, WAYBEL_0:def_15; hence contradiction ; ::_thesis: verum end; cluster uparrow X -> empty ; coherence uparrow X is empty proof assume not uparrow X is empty ; ::_thesis: contradiction then consider x being set such that A2: x in uparrow X by XBOOLE_0:def_1; reconsider x = x as Element of L by A2; ex z being Element of L st ( z <= x & z in X ) by A2, WAYBEL_0:def_16; hence contradiction ; ::_thesis: verum end; end; theorem Th1: :: YELLOW_3:1 for X, Y being set for D being Subset of [:X,Y:] holds D c= [:(proj1 D),(proj2 D):] proof let X, Y be set ; ::_thesis: for D being Subset of [:X,Y:] holds D c= [:(proj1 D),(proj2 D):] let D be Subset of [:X,Y:]; ::_thesis: D c= [:(proj1 D),(proj2 D):] let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in D or q in [:(proj1 D),(proj2 D):] ) assume A1: q in D ; ::_thesis: q in [:(proj1 D),(proj2 D):] then consider x, y being set such that x in X and y in Y and A2: q = [x,y] by ZFMISC_1:def_2; ( x in proj1 D & y in proj2 D ) by A1, A2, XTUPLE_0:def_12, XTUPLE_0:def_13; hence q in [:(proj1 D),(proj2 D):] by A2, ZFMISC_1:def_2; ::_thesis: verum end; Lm1: for x, a1, a2, b1, b2 being set st x = [[a1,a2],[b1,b2]] holds ( (x `1) `1 = a1 & (x `1) `2 = a2 & (x `2) `1 = b1 & (x `2) `2 = b2 ) proof let x, a1, a2, b1, b2 be set ; ::_thesis: ( x = [[a1,a2],[b1,b2]] implies ( (x `1) `1 = a1 & (x `1) `2 = a2 & (x `2) `1 = b1 & (x `2) `2 = b2 ) ) assume x = [[a1,a2],[b1,b2]] ; ::_thesis: ( (x `1) `1 = a1 & (x `1) `2 = a2 & (x `2) `1 = b1 & (x `2) `2 = b2 ) then ( x `1 = [a1,a2] & x `2 = [b1,b2] ) by MCART_1:7; hence ( (x `1) `1 = a1 & (x `1) `2 = a2 & (x `2) `1 = b1 & (x `2) `2 = b2 ) by MCART_1:7; ::_thesis: verum end; theorem :: YELLOW_3:2 for L being transitive antisymmetric with_infima RelStr for a, b, c, d being Element of L st a <= c & b <= d holds a "/\" b <= c "/\" d proof let L be transitive antisymmetric with_infima RelStr ; ::_thesis: for a, b, c, d being Element of L st a <= c & b <= d holds a "/\" b <= c "/\" d let a, b, c, d be Element of L; ::_thesis: ( a <= c & b <= d implies a "/\" b <= c "/\" d ) assume that A1: a <= c and A2: b <= d ; ::_thesis: a "/\" b <= c "/\" d A3: ex_inf_of {a,b},L by YELLOW_0:21; then a "/\" b <= b by YELLOW_0:19; then A4: a "/\" b <= d by A2, ORDERS_2:3; a "/\" b <= a by A3, YELLOW_0:19; then ( ex x being Element of L st ( c >= x & d >= x & ( for z being Element of L st c >= z & d >= z holds x >= z ) ) & a "/\" b <= c ) by A1, LATTICE3:def_11, ORDERS_2:3; hence a "/\" b <= c "/\" d by A4, LATTICE3:def_14; ::_thesis: verum end; theorem :: YELLOW_3:3 for L being transitive antisymmetric with_suprema RelStr for a, b, c, d being Element of L st a <= c & b <= d holds a "\/" b <= c "\/" d proof let L be transitive antisymmetric with_suprema RelStr ; ::_thesis: for a, b, c, d being Element of L st a <= c & b <= d holds a "\/" b <= c "\/" d let a, b, c, d be Element of L; ::_thesis: ( a <= c & b <= d implies a "\/" b <= c "\/" d ) assume that A1: a <= c and A2: b <= d ; ::_thesis: a "\/" b <= c "\/" d A3: ex_sup_of {c,d},L by YELLOW_0:20; then d <= c "\/" d by YELLOW_0:18; then A4: b <= c "\/" d by A2, ORDERS_2:3; c <= c "\/" d by A3, YELLOW_0:18; then ( ex x being Element of L st ( a <= x & b <= x & ( for z being Element of L st a <= z & b <= z holds x <= z ) ) & a <= c "\/" d ) by A1, LATTICE3:def_10, ORDERS_2:3; hence a "\/" b <= c "\/" d by A4, LATTICE3:def_13; ::_thesis: verum end; theorem :: YELLOW_3:4 for L being non empty reflexive antisymmetric complete RelStr for D being Subset of L for x being Element of L st x in D holds (sup D) "/\" x = x proof let L be non empty reflexive antisymmetric complete RelStr ; ::_thesis: for D being Subset of L for x being Element of L st x in D holds (sup D) "/\" x = x let D be Subset of L; ::_thesis: for x being Element of L st x in D holds (sup D) "/\" x = x let x be Element of L; ::_thesis: ( x in D implies (sup D) "/\" x = x ) assume A1: x in D ; ::_thesis: (sup D) "/\" x = x D is_<=_than sup D by YELLOW_0:32; then x <= sup D by A1, LATTICE3:def_9; hence (sup D) "/\" x = x by YELLOW_0:25; ::_thesis: verum end; theorem :: YELLOW_3:5 for L being non empty reflexive antisymmetric complete RelStr for D being Subset of L for x being Element of L st x in D holds (inf D) "\/" x = x proof let L be non empty reflexive antisymmetric complete RelStr ; ::_thesis: for D being Subset of L for x being Element of L st x in D holds (inf D) "\/" x = x let D be Subset of L; ::_thesis: for x being Element of L st x in D holds (inf D) "\/" x = x let x be Element of L; ::_thesis: ( x in D implies (inf D) "\/" x = x ) assume A1: x in D ; ::_thesis: (inf D) "\/" x = x D is_>=_than inf D by YELLOW_0:33; then inf D <= x by A1, LATTICE3:def_8; hence (inf D) "\/" x = x by YELLOW_0:24; ::_thesis: verum end; theorem :: YELLOW_3:6 for L being RelStr for X, Y being Subset of L st X c= Y holds downarrow X c= downarrow Y proof let L be RelStr ; ::_thesis: for X, Y being Subset of L st X c= Y holds downarrow X c= downarrow Y let X, Y be Subset of L; ::_thesis: ( X c= Y implies downarrow X c= downarrow Y ) assume A1: X c= Y ; ::_thesis: downarrow X c= downarrow Y let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in downarrow X or q in downarrow Y ) assume A2: q in downarrow X ; ::_thesis: q in downarrow Y then reconsider x = q as Element of L ; ex z being Element of L st ( x <= z & z in X ) by A2, WAYBEL_0:def_15; hence q in downarrow Y by A1, WAYBEL_0:def_15; ::_thesis: verum end; theorem :: YELLOW_3:7 for L being RelStr for X, Y being Subset of L st X c= Y holds uparrow X c= uparrow Y proof let L be RelStr ; ::_thesis: for X, Y being Subset of L st X c= Y holds uparrow X c= uparrow Y let X, Y be Subset of L; ::_thesis: ( X c= Y implies uparrow X c= uparrow Y ) assume A1: X c= Y ; ::_thesis: uparrow X c= uparrow Y let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in uparrow X or q in uparrow Y ) assume A2: q in uparrow X ; ::_thesis: q in uparrow Y then reconsider x = q as Element of L ; ex z being Element of L st ( z <= x & z in X ) by A2, WAYBEL_0:def_16; hence q in uparrow Y by A1, WAYBEL_0:def_16; ::_thesis: verum end; theorem :: YELLOW_3:8 for S, T being with_infima Poset for f being Function of S,T for x, y being Element of S holds ( f preserves_inf_of {x,y} iff f . (x "/\" y) = (f . x) "/\" (f . y) ) proof let S, T be with_infima Poset; ::_thesis: for f being Function of S,T for x, y being Element of S holds ( f preserves_inf_of {x,y} iff f . (x "/\" y) = (f . x) "/\" (f . y) ) let f be Function of S,T; ::_thesis: for x, y being Element of S holds ( f preserves_inf_of {x,y} iff f . (x "/\" y) = (f . x) "/\" (f . y) ) let x, y be Element of S; ::_thesis: ( f preserves_inf_of {x,y} iff f . (x "/\" y) = (f . x) "/\" (f . y) ) A1: dom f = the carrier of S by FUNCT_2:def_1; hereby ::_thesis: ( f . (x "/\" y) = (f . x) "/\" (f . y) implies f preserves_inf_of {x,y} ) A2: ex_inf_of {x,y},S by YELLOW_0:21; assume A3: f preserves_inf_of {x,y} ; ::_thesis: f . (x "/\" y) = (f . x) "/\" (f . y) thus f . (x "/\" y) = f . (inf {x,y}) by YELLOW_0:40 .= inf (f .: {x,y}) by A3, A2, WAYBEL_0:def_30 .= inf {(f . x),(f . y)} by A1, FUNCT_1:60 .= (f . x) "/\" (f . y) by YELLOW_0:40 ; ::_thesis: verum end; assume A4: f . (x "/\" y) = (f . x) "/\" (f . y) ; ::_thesis: f preserves_inf_of {x,y} assume ex_inf_of {x,y},S ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of f .: {x,y},T & "/\" ((f .: {x,y}),T) = f . ("/\" ({x,y},S)) ) f .: {x,y} = {(f . x),(f . y)} by A1, FUNCT_1:60; hence ex_inf_of f .: {x,y},T by YELLOW_0:21; ::_thesis: "/\" ((f .: {x,y}),T) = f . ("/\" ({x,y},S)) thus inf (f .: {x,y}) = inf {(f . x),(f . y)} by A1, FUNCT_1:60 .= (f . x) "/\" (f . y) by YELLOW_0:40 .= f . (inf {x,y}) by A4, YELLOW_0:40 ; ::_thesis: verum end; theorem :: YELLOW_3:9 for S, T being with_suprema Poset for f being Function of S,T for x, y being Element of S holds ( f preserves_sup_of {x,y} iff f . (x "\/" y) = (f . x) "\/" (f . y) ) proof let S, T be with_suprema Poset; ::_thesis: for f being Function of S,T for x, y being Element of S holds ( f preserves_sup_of {x,y} iff f . (x "\/" y) = (f . x) "\/" (f . y) ) let f be Function of S,T; ::_thesis: for x, y being Element of S holds ( f preserves_sup_of {x,y} iff f . (x "\/" y) = (f . x) "\/" (f . y) ) let x, y be Element of S; ::_thesis: ( f preserves_sup_of {x,y} iff f . (x "\/" y) = (f . x) "\/" (f . y) ) A1: dom f = the carrier of S by FUNCT_2:def_1; hereby ::_thesis: ( f . (x "\/" y) = (f . x) "\/" (f . y) implies f preserves_sup_of {x,y} ) A2: ex_sup_of {x,y},S by YELLOW_0:20; assume A3: f preserves_sup_of {x,y} ; ::_thesis: f . (x "\/" y) = (f . x) "\/" (f . y) thus f . (x "\/" y) = f . (sup {x,y}) by YELLOW_0:41 .= sup (f .: {x,y}) by A3, A2, WAYBEL_0:def_31 .= sup {(f . x),(f . y)} by A1, FUNCT_1:60 .= (f . x) "\/" (f . y) by YELLOW_0:41 ; ::_thesis: verum end; assume A4: f . (x "\/" y) = (f . x) "\/" (f . y) ; ::_thesis: f preserves_sup_of {x,y} assume ex_sup_of {x,y},S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of f .: {x,y},T & "\/" ((f .: {x,y}),T) = f . ("\/" ({x,y},S)) ) f .: {x,y} = {(f . x),(f . y)} by A1, FUNCT_1:60; hence ex_sup_of f .: {x,y},T by YELLOW_0:20; ::_thesis: "\/" ((f .: {x,y}),T) = f . ("\/" ({x,y},S)) thus sup (f .: {x,y}) = sup {(f . x),(f . y)} by A1, FUNCT_1:60 .= (f . x) "\/" (f . y) by YELLOW_0:41 .= f . (sup {x,y}) by A4, YELLOW_0:41 ; ::_thesis: verum end; scheme :: YELLOW_3:sch 2 InfUnion{ F1() -> non empty antisymmetric complete RelStr , P1[ set ] } : "/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) >= "/\" ((union { X where X is Subset of F1() : P1[X] } ),F1()) proof "/\" ((union { X where X is Subset of F1() : P1[X] } ),F1()) is_<=_than { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } proof let a be Element of F1(); :: according to LATTICE3:def_8 ::_thesis: ( not a in { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } or "/\" ((union { X where X is Subset of F1() : P1[X] } ),F1()) <= a ) assume a in { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ; ::_thesis: "/\" ((union { X where X is Subset of F1() : P1[X] } ),F1()) <= a then consider q being Subset of F1() such that A1: a = "/\" (q,F1()) and A2: P1[q] ; A3: ( ex_inf_of q,F1() & ex_inf_of union { X where X is Subset of F1() : P1[X] } ,F1() ) by YELLOW_0:17; q in { X where X is Subset of F1() : P1[X] } by A2; hence "/\" ((union { X where X is Subset of F1() : P1[X] } ),F1()) <= a by A1, A3, YELLOW_0:35, ZFMISC_1:74; ::_thesis: verum end; hence "/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) >= "/\" ((union { X where X is Subset of F1() : P1[X] } ),F1()) by YELLOW_0:33; ::_thesis: verum end; scheme :: YELLOW_3:sch 3 InfofInfs{ F1() -> complete LATTICE, P1[ set ] } : "/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) = "/\" ((union { X where X is Subset of F1() : P1[X] } ),F1()) proof union { X where X is Subset of F1() : P1[X] } is_>=_than "/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) proof let a be Element of F1(); :: according to LATTICE3:def_8 ::_thesis: ( not a in union { X where X is Subset of F1() : P1[X] } or "/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) <= a ) assume a in union { X where X is Subset of F1() : P1[X] } ; ::_thesis: "/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) <= a then consider b being set such that A1: a in b and A2: b in { X where X is Subset of F1() : P1[X] } by TARSKI:def_4; consider c being Subset of F1() such that A3: b = c and A4: P1[c] by A2; "/\" (c,F1()) in { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } by A4; then A5: "/\" (c,F1()) >= "/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) by YELLOW_2:22; "/\" (c,F1()) <= a by A1, A3, YELLOW_2:22; hence "/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) <= a by A5, YELLOW_0:def_2; ::_thesis: verum end; then A6: "/\" ((union { X where X is Subset of F1() : P1[X] } ),F1()) >= "/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) by YELLOW_0:33; "/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) >= "/\" ((union { X where X is Subset of F1() : P1[X] } ),F1()) from YELLOW_3:sch_2(); hence "/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) = "/\" ((union { X where X is Subset of F1() : P1[X] } ),F1()) by A6, ORDERS_2:2; ::_thesis: verum end; scheme :: YELLOW_3:sch 4 SupUnion{ F1() -> non empty antisymmetric complete RelStr , P1[ set ] } : "\/" ( { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) <= "\/" ((union { X where X is Subset of F1() : P1[X] } ),F1()) proof A1: "\/" ((union { X where X is Subset of F1() : P1[X] } ),F1()) is_>=_than { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } proof let a be Element of F1(); :: according to LATTICE3:def_9 ::_thesis: ( not a in { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } or a <= "\/" ((union { X where X is Subset of F1() : P1[X] } ),F1()) ) assume a in { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ; ::_thesis: a <= "\/" ((union { X where X is Subset of F1() : P1[X] } ),F1()) then consider q being Subset of F1() such that A2: a = "\/" (q,F1()) and A3: P1[q] ; A4: ( ex_sup_of q,F1() & ex_sup_of union { X where X is Subset of F1() : P1[X] } ,F1() ) by YELLOW_0:17; q in { X where X is Subset of F1() : P1[X] } by A3; hence a <= "\/" ((union { X where X is Subset of F1() : P1[X] } ),F1()) by A2, A4, YELLOW_0:34, ZFMISC_1:74; ::_thesis: verum end; ex_sup_of { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ,F1() by YELLOW_0:17; hence "\/" ( { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) <= "\/" ((union { X where X is Subset of F1() : P1[X] } ),F1()) by A1, YELLOW_0:def_9; ::_thesis: verum end; scheme :: YELLOW_3:sch 5 SupofSups{ F1() -> complete LATTICE, P1[ set ] } : "\/" ( { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) = "\/" ((union { X where X is Subset of F1() : P1[X] } ),F1()) proof A1: union { X where X is Subset of F1() : P1[X] } is_<=_than "\/" ( { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) proof let a be Element of F1(); :: according to LATTICE3:def_9 ::_thesis: ( not a in union { X where X is Subset of F1() : P1[X] } or a <= "\/" ( { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) ) assume a in union { X where X is Subset of F1() : P1[X] } ; ::_thesis: a <= "\/" ( { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) then consider b being set such that A2: a in b and A3: b in { X where X is Subset of F1() : P1[X] } by TARSKI:def_4; consider c being Subset of F1() such that A4: b = c and A5: P1[c] by A3; "\/" (c,F1()) in { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } by A5; then A6: "\/" (c,F1()) <= "\/" ( { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) by YELLOW_2:22; a <= "\/" (c,F1()) by A2, A4, YELLOW_2:22; hence a <= "\/" ( { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) by A6, YELLOW_0:def_2; ::_thesis: verum end; A7: "\/" ( { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) <= "\/" ((union { X where X is Subset of F1() : P1[X] } ),F1()) from YELLOW_3:sch_4(); ex_sup_of union { X where X is Subset of F1() : P1[X] } ,F1() by YELLOW_0:17; then "\/" ((union { X where X is Subset of F1() : P1[X] } ),F1()) <= "\/" ( { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) by A1, YELLOW_0:def_9; hence "\/" ( { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) = "\/" ((union { X where X is Subset of F1() : P1[X] } ),F1()) by A7, ORDERS_2:2; ::_thesis: verum end; begin definition let P, R be Relation; func["P,R"] -> Relation means :Def1: :: YELLOW_3:def 1 for x, y being set holds ( [x,y] in it iff ex p, q, s, t being set st ( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ); existence ex b1 being Relation st for x, y being set holds ( [x,y] in b1 iff ex p, q, s, t being set st ( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ) proof defpred S1[ set , set ] means ex p, s, q, t being set st ( $1 = [p,q] & $2 = [s,t] & [p,s] in P & [q,t] in R ); consider Q being Relation such that A1: for x, y being set holds ( [x,y] in Q iff ( x in [:(dom P),(dom R):] & y in [:(rng P),(rng R):] & S1[x,y] ) ) from RELAT_1:sch_1(); take Q ; ::_thesis: for x, y being set holds ( [x,y] in Q iff ex p, q, s, t being set st ( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ) let x, y be set ; ::_thesis: ( [x,y] in Q iff ex p, q, s, t being set st ( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ) hereby ::_thesis: ( ex p, q, s, t being set st ( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) implies [x,y] in Q ) assume [x,y] in Q ; ::_thesis: ex p, q, s, t being set st ( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) then consider p, s, q, t being set such that A2: ( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) by A1; take p = p; ::_thesis: ex q, s, t being set st ( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) take q = q; ::_thesis: ex s, t being set st ( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) take s = s; ::_thesis: ex t being set st ( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) take t = t; ::_thesis: ( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) thus ( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) by A2; ::_thesis: verum end; given p, q, s, t being set such that A3: x = [p,q] and A4: y = [s,t] and A5: ( [p,s] in P & [q,t] in R ) ; ::_thesis: [x,y] in Q ( s in rng P & t in rng R ) by A5, XTUPLE_0:def_13; then A6: y in [:(rng P),(rng R):] by A4, ZFMISC_1:87; ( p in dom P & q in dom R ) by A5, XTUPLE_0:def_12; then x in [:(dom P),(dom R):] by A3, ZFMISC_1:87; hence [x,y] in Q by A1, A3, A4, A5, A6; ::_thesis: verum end; uniqueness for b1, b2 being Relation st ( for x, y being set holds ( [x,y] in b1 iff ex p, q, s, t being set st ( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ) ) & ( for x, y being set holds ( [x,y] in b2 iff ex p, q, s, t being set st ( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ) ) holds b1 = b2 proof defpred S1[ set , set ] means ex p, q, s, t being set st ( $1 = [p,q] & $2 = [s,t] & [p,s] in P & [q,t] in R ); let A, B be Relation; ::_thesis: ( ( for x, y being set holds ( [x,y] in A iff ex p, q, s, t being set st ( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ) ) & ( for x, y being set holds ( [x,y] in B iff ex p, q, s, t being set st ( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ) ) implies A = B ) assume that A7: for x, y being set holds ( [x,y] in A iff S1[x,y] ) and A8: for x, y being set holds ( [x,y] in B iff S1[x,y] ) ; ::_thesis: A = B thus A = B from RELAT_1:sch_2(A7, A8); ::_thesis: verum end; end; :: deftheorem Def1 defines [" YELLOW_3:def_1_:_ for P, R, b3 being Relation holds ( b3 = ["P,R"] iff for x, y being set holds ( [x,y] in b3 iff ex p, q, s, t being set st ( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ) ); theorem Th10: :: YELLOW_3:10 for P, R being Relation for x being set holds ( x in ["P,R"] iff ( [((x `1) `1),((x `2) `1)] in P & [((x `1) `2),((x `2) `2)] in R & ex a, b being set st x = [a,b] & ex c, d being set st x `1 = [c,d] & ex e, f being set st x `2 = [e,f] ) ) proof let P, R be Relation; ::_thesis: for x being set holds ( x in ["P,R"] iff ( [((x `1) `1),((x `2) `1)] in P & [((x `1) `2),((x `2) `2)] in R & ex a, b being set st x = [a,b] & ex c, d being set st x `1 = [c,d] & ex e, f being set st x `2 = [e,f] ) ) let x be set ; ::_thesis: ( x in ["P,R"] iff ( [((x `1) `1),((x `2) `1)] in P & [((x `1) `2),((x `2) `2)] in R & ex a, b being set st x = [a,b] & ex c, d being set st x `1 = [c,d] & ex e, f being set st x `2 = [e,f] ) ) hereby ::_thesis: ( [((x `1) `1),((x `2) `1)] in P & [((x `1) `2),((x `2) `2)] in R & ex a, b being set st x = [a,b] & ex c, d being set st x `1 = [c,d] & ex e, f being set st x `2 = [e,f] implies x in ["P,R"] ) assume A1: x in ["P,R"] ; ::_thesis: ( [((x `1) `1),((x `2) `1)] in P & [((x `1) `2),((x `2) `2)] in R & ex a, b being set st x = [a,b] & ex c, d being set st x `1 = [c,d] & ex e, f being set st x `2 = [e,f] ) then consider y, z being set such that A2: x = [y,z] by RELAT_1:def_1; consider p, q, s, t being set such that A3: y = [p,q] and A4: z = [s,t] and A5: ( [p,s] in P & [q,t] in R ) by A1, A2, Def1; ( (x `1) `1 = p & (x `1) `2 = q ) by A2, A3, A4, Lm1; hence ( [((x `1) `1),((x `2) `1)] in P & [((x `1) `2),((x `2) `2)] in R ) by A2, A3, A4, A5, Lm1; ::_thesis: ( ex a, b being set st x = [a,b] & ex c, d being set st x `1 = [c,d] & ex e, f being set st x `2 = [e,f] ) thus ex a, b being set st x = [a,b] by A2; ::_thesis: ( ex c, d being set st x `1 = [c,d] & ex e, f being set st x `2 = [e,f] ) thus ex c, d being set st x `1 = [c,d] by A2, A3, MCART_1:7; ::_thesis: ex e, f being set st x `2 = [e,f] thus ex e, f being set st x `2 = [e,f] by A2, A4, MCART_1:7; ::_thesis: verum end; assume that A6: [((x `1) `1),((x `2) `1)] in P and A7: [((x `1) `2),((x `2) `2)] in R and A8: ex a, b being set st x = [a,b] and A9: ex c, d being set st x `1 = [c,d] and A10: ex e, f being set st x `2 = [e,f] ; ::_thesis: x in ["P,R"] consider c, d being set such that A11: x `1 = [c,d] by A9; consider e, f being set such that A12: x `2 = [e,f] by A10; [c,((x `2) `1)] in P by A6, A11, MCART_1:7; then A13: [c,e] in P by A12, MCART_1:7; consider a, b being set such that A14: x = [a,b] by A8; [d,((x `2) `2)] in R by A7, A11, MCART_1:7; then A15: [d,f] in R by A12, MCART_1:7; A16: b = [e,f] by A14, A12, MCART_1:7; a = [c,d] by A14, A11, MCART_1:7; hence x in ["P,R"] by A14, A16, A13, A15, Def1; ::_thesis: verum end; definition let A, B, X, Y be set ; let P be Relation of A,B; let R be Relation of X,Y; :: original: [" redefine func["P,R"] -> Relation of [:A,X:],[:B,Y:]; coherence ["P,R"] is Relation of [:A,X:],[:B,Y:] proof ["P,R"] c= [:[:A,X:],[:B,Y:]:] proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in ["P,R"] or q in [:[:A,X:],[:B,Y:]:] ) assume A1: q in ["P,R"] ; ::_thesis: q in [:[:A,X:],[:B,Y:]:] then consider a, b being set such that A2: q = [a,b] by Th10; [((q `1) `2),((q `2) `2)] in R by A1, Th10; then consider s, t being set such that A3: [((q `1) `2),((q `2) `2)] = [s,t] and A4: s in X and A5: t in Y by RELSET_1:2; consider a2, b2 being set such that A6: q `2 = [a2,b2] by A1, Th10; [((q `1) `1),((q `2) `1)] in P by A1, Th10; then consider x, y being set such that A7: [((q `1) `1),((q `2) `1)] = [x,y] and A8: x in A and A9: y in B by RELSET_1:2; consider a1, b1 being set such that A10: q `1 = [a1,b1] by A1, Th10; A11: b = [a2,b2] by A2, A6, MCART_1:7; then A12: b `2 = t by A3, A6, XTUPLE_0:1; A13: a = [a1,b1] by A2, A10, MCART_1:7; then A14: a `2 = s by A3, A10, XTUPLE_0:1; b `1 = y by A7, A6, A11, XTUPLE_0:1; then A15: b in [:B,Y:] by A9, A5, A11, A12, MCART_1:11; a `1 = x by A7, A10, A13, XTUPLE_0:1; then a in [:A,X:] by A8, A4, A13, A14, MCART_1:11; hence q in [:[:A,X:],[:B,Y:]:] by A2, A15, ZFMISC_1:def_2; ::_thesis: verum end; hence ["P,R"] is Relation of [:A,X:],[:B,Y:] ; ::_thesis: verum end; end; definition let X, Y be RelStr ; func[:X,Y:] -> strict RelStr means :Def2: :: YELLOW_3:def 2 ( the carrier of it = [: the carrier of X, the carrier of Y:] & the InternalRel of it = [" the InternalRel of X, the InternalRel of Y"] ); existence ex b1 being strict RelStr st ( the carrier of b1 = [: the carrier of X, the carrier of Y:] & the InternalRel of b1 = [" the InternalRel of X, the InternalRel of Y"] ) proof take RelStr(# [: the carrier of X, the carrier of Y:],[" the InternalRel of X, the InternalRel of Y"] #) ; ::_thesis: ( the carrier of RelStr(# [: the carrier of X, the carrier of Y:],[" the InternalRel of X, the InternalRel of Y"] #) = [: the carrier of X, the carrier of Y:] & the InternalRel of RelStr(# [: the carrier of X, the carrier of Y:],[" the InternalRel of X, the InternalRel of Y"] #) = [" the InternalRel of X, the InternalRel of Y"] ) thus ( the carrier of RelStr(# [: the carrier of X, the carrier of Y:],[" the InternalRel of X, the InternalRel of Y"] #) = [: the carrier of X, the carrier of Y:] & the InternalRel of RelStr(# [: the carrier of X, the carrier of Y:],[" the InternalRel of X, the InternalRel of Y"] #) = [" the InternalRel of X, the InternalRel of Y"] ) ; ::_thesis: verum end; uniqueness for b1, b2 being strict RelStr st the carrier of b1 = [: the carrier of X, the carrier of Y:] & the InternalRel of b1 = [" the InternalRel of X, the InternalRel of Y"] & the carrier of b2 = [: the carrier of X, the carrier of Y:] & the InternalRel of b2 = [" the InternalRel of X, the InternalRel of Y"] holds b1 = b2 ; end; :: deftheorem Def2 defines [: YELLOW_3:def_2_:_ for X, Y being RelStr for b3 being strict RelStr holds ( b3 = [:X,Y:] iff ( the carrier of b3 = [: the carrier of X, the carrier of Y:] & the InternalRel of b3 = [" the InternalRel of X, the InternalRel of Y"] ) ); definition let L1, L2 be RelStr ; let D be Subset of [:L1,L2:]; :: original: proj1 redefine func proj1 D -> Subset of L1; coherence proj1 D is Subset of L1 proof proj1 D c= the carrier of L1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in proj1 D or x in the carrier of L1 ) assume x in proj1 D ; ::_thesis: x in the carrier of L1 then A1: ex y being set st [x,y] in D by XTUPLE_0:def_12; the carrier of [:L1,L2:] = [: the carrier of L1, the carrier of L2:] by Def2; hence x in the carrier of L1 by A1, ZFMISC_1:87; ::_thesis: verum end; hence proj1 D is Subset of L1 ; ::_thesis: verum end; :: original: proj2 redefine func proj2 D -> Subset of L2; coherence proj2 D is Subset of L2 proof proj2 D c= the carrier of L2 proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in proj2 D or y in the carrier of L2 ) assume y in proj2 D ; ::_thesis: y in the carrier of L2 then A2: ex x being set st [x,y] in D by XTUPLE_0:def_13; the carrier of [:L1,L2:] = [: the carrier of L1, the carrier of L2:] by Def2; hence y in the carrier of L2 by A2, ZFMISC_1:87; ::_thesis: verum end; hence proj2 D is Subset of L2 ; ::_thesis: verum end; end; definition let S1, S2 be RelStr ; let D1 be Subset of S1; let D2 be Subset of S2; :: original: [: redefine func[:D1,D2:] -> Subset of [:S1,S2:]; coherence [:D1,D2:] is Subset of [:S1,S2:] proof [:D1,D2:] c= [: the carrier of S1, the carrier of S2:] ; hence [:D1,D2:] is Subset of [:S1,S2:] by Def2; ::_thesis: verum end; end; definition let S1, S2 be non empty RelStr ; let x be Element of S1; let y be Element of S2; :: original: [ redefine func[x,y] -> Element of [:S1,S2:]; coherence [x,y] is Element of [:S1,S2:] proof reconsider y1 = y as Element of S2 ; reconsider x1 = x as Element of S1 ; [x1,y1] is Element of [:S1,S2:] by Def2; hence [x,y] is Element of [:S1,S2:] ; ::_thesis: verum end; end; definition let L1, L2 be non empty RelStr ; let x be Element of [:L1,L2:]; :: original: `1 redefine funcx `1 -> Element of L1; coherence x `1 is Element of L1 proof the carrier of [:L1,L2:] = [: the carrier of L1, the carrier of L2:] by Def2; hence x `1 is Element of L1 by MCART_1:10; ::_thesis: verum end; :: original: `2 redefine funcx `2 -> Element of L2; coherence x `2 is Element of L2 proof the carrier of [:L1,L2:] = [: the carrier of L1, the carrier of L2:] by Def2; hence x `2 is Element of L2 by MCART_1:10; ::_thesis: verum end; end; theorem Th11: :: YELLOW_3:11 for S1, S2 being non empty RelStr for a, c being Element of S1 for b, d being Element of S2 holds ( ( a <= c & b <= d ) iff [a,b] <= [c,d] ) proof let S1, S2 be non empty RelStr ; ::_thesis: for a, c being Element of S1 for b, d being Element of S2 holds ( ( a <= c & b <= d ) iff [a,b] <= [c,d] ) let a, c be Element of S1; ::_thesis: for b, d being Element of S2 holds ( ( a <= c & b <= d ) iff [a,b] <= [c,d] ) let b, d be Element of S2; ::_thesis: ( ( a <= c & b <= d ) iff [a,b] <= [c,d] ) set I1 = the InternalRel of S1; set I2 = the InternalRel of S2; set x = [[a,b],[c,d]]; A1: ( ([[a,b],[c,d]] `1) `1 = a & ([[a,b],[c,d]] `2) `1 = c ) ; A2: ( ([[a,b],[c,d]] `1) `2 = b & ([[a,b],[c,d]] `2) `2 = d ) ; thus ( a <= c & b <= d implies [a,b] <= [c,d] ) ::_thesis: ( [a,b] <= [c,d] implies ( a <= c & b <= d ) ) proof assume ( a <= c & b <= d ) ; ::_thesis: [a,b] <= [c,d] then ( [(([[a,b],[c,d]] `1) `1),(([[a,b],[c,d]] `2) `1)] in the InternalRel of S1 & [(([[a,b],[c,d]] `1) `2),(([[a,b],[c,d]] `2) `2)] in the InternalRel of S2 ) by ORDERS_2:def_5; then [[a,b],[c,d]] in [" the InternalRel of S1, the InternalRel of S2"] by Th10; hence [[a,b],[c,d]] in the InternalRel of [:S1,S2:] by Def2; :: according to ORDERS_2:def_5 ::_thesis: verum end; assume [a,b] <= [c,d] ; ::_thesis: ( a <= c & b <= d ) then [[a,b],[c,d]] in the InternalRel of [:S1,S2:] by ORDERS_2:def_5; then [[a,b],[c,d]] in [" the InternalRel of S1, the InternalRel of S2"] by Def2; hence ( [a,c] in the InternalRel of S1 & [b,d] in the InternalRel of S2 ) by A1, A2, Th10; :: according to ORDERS_2:def_5 ::_thesis: verum end; theorem Th12: :: YELLOW_3:12 for S1, S2 being non empty RelStr for x, y being Element of [:S1,S2:] holds ( x <= y iff ( x `1 <= y `1 & x `2 <= y `2 ) ) proof let S1, S2 be non empty RelStr ; ::_thesis: for x, y being Element of [:S1,S2:] holds ( x <= y iff ( x `1 <= y `1 & x `2 <= y `2 ) ) let x, y be Element of [:S1,S2:]; ::_thesis: ( x <= y iff ( x `1 <= y `1 & x `2 <= y `2 ) ) A1: the carrier of [:S1,S2:] = [: the carrier of S1, the carrier of S2:] by Def2; then ex c, d being set st ( c in the carrier of S1 & d in the carrier of S2 & y = [c,d] ) by ZFMISC_1:def_2; then A2: y = [(y `1),(y `2)] by MCART_1:8; ex a, b being set st ( a in the carrier of S1 & b in the carrier of S2 & x = [a,b] ) by A1, ZFMISC_1:def_2; then x = [(x `1),(x `2)] by MCART_1:8; hence ( x <= y iff ( x `1 <= y `1 & x `2 <= y `2 ) ) by A2, Th11; ::_thesis: verum end; theorem :: YELLOW_3:13 for A, B being RelStr for C being non empty RelStr for f, g being Function of [:A,B:],C st ( for x being Element of A for y being Element of B holds f . (x,y) = g . (x,y) ) holds f = g proof let A, B be RelStr ; ::_thesis: for C being non empty RelStr for f, g being Function of [:A,B:],C st ( for x being Element of A for y being Element of B holds f . (x,y) = g . (x,y) ) holds f = g let C be non empty RelStr ; ::_thesis: for f, g being Function of [:A,B:],C st ( for x being Element of A for y being Element of B holds f . (x,y) = g . (x,y) ) holds f = g let f, g be Function of [:A,B:],C; ::_thesis: ( ( for x being Element of A for y being Element of B holds f . (x,y) = g . (x,y) ) implies f = g ) assume for x being Element of A for y being Element of B holds f . (x,y) = g . (x,y) ; ::_thesis: f = g then A1: for x, y being set st x in the carrier of A & y in the carrier of B holds f . (x,y) = g . (x,y) ; the carrier of [:A,B:] = [: the carrier of A, the carrier of B:] by Def2; hence f = g by A1, BINOP_1:1; ::_thesis: verum end; registration let X, Y be non empty RelStr ; cluster[:X,Y:] -> non empty strict ; coherence not [:X,Y:] is empty proof set y = the Element of Y; set x = the Element of X; [ the Element of X, the Element of Y] in [: the carrier of X, the carrier of Y:] by ZFMISC_1:87; hence not [:X,Y:] is empty by Def2; ::_thesis: verum end; end; registration let X, Y be reflexive RelStr ; cluster[:X,Y:] -> strict reflexive ; coherence [:X,Y:] is reflexive proof let x be set ; :: according to RELAT_2:def_1,ORDERS_2:def_2 ::_thesis: ( not x in the carrier of [:X,Y:] or [x,x] in the InternalRel of [:X,Y:] ) assume x in the carrier of [:X,Y:] ; ::_thesis: [x,x] in the InternalRel of [:X,Y:] then x in [: the carrier of X, the carrier of Y:] by Def2; then consider x1, x2 being set such that A1: x1 in the carrier of X and A2: x2 in the carrier of Y and A3: x = [x1,x2] by ZFMISC_1:def_2; the InternalRel of X is_reflexive_in the carrier of X by ORDERS_2:def_2; then A4: [x1,x1] in the InternalRel of X by A1, RELAT_2:def_1; the InternalRel of Y is_reflexive_in the carrier of Y by ORDERS_2:def_2; then A5: [x2,x2] in the InternalRel of Y by A2, RELAT_2:def_1; set a = [[x1,x2],[x1,x2]]; A6: ( [[x1,x2],[x1,x2]] `1 = [x1,x2] & [[x1,x2],[x1,x2]] `2 = [x1,x2] ) ; ( ([[x1,x2],[x1,x2]] `1) `1 = x1 & ([[x1,x2],[x1,x2]] `1) `2 = x2 ) ; then [x,x] in [" the InternalRel of X, the InternalRel of Y"] by A3, A4, A5, A6, Th10; hence [x,x] in the InternalRel of [:X,Y:] by Def2; ::_thesis: verum end; end; registration let X, Y be antisymmetric RelStr ; cluster[:X,Y:] -> strict antisymmetric ; coherence [:X,Y:] is antisymmetric proof let x, y be set ; :: according to RELAT_2:def_4,ORDERS_2:def_4 ::_thesis: ( not x in the carrier of [:X,Y:] or not y in the carrier of [:X,Y:] or not [x,y] in the InternalRel of [:X,Y:] or not [y,x] in the InternalRel of [:X,Y:] or x = y ) assume that A1: x in the carrier of [:X,Y:] and A2: y in the carrier of [:X,Y:] and A3: [x,y] in the InternalRel of [:X,Y:] and A4: [y,x] in the InternalRel of [:X,Y:] ; ::_thesis: x = y x in [: the carrier of X, the carrier of Y:] by A1, Def2; then consider x1, x2 being set such that A5: x1 in the carrier of X and A6: x2 in the carrier of Y and A7: x = [x1,x2] by ZFMISC_1:def_2; y in [: the carrier of X, the carrier of Y:] by A2, Def2; then consider y1, y2 being set such that A8: y1 in the carrier of X and A9: y2 in the carrier of Y and A10: y = [y1,y2] by ZFMISC_1:def_2; A11: [y,x] in [" the InternalRel of X, the InternalRel of Y"] by A4, Def2; then [(([y,x] `1) `1),(([y,x] `2) `1)] in the InternalRel of X by Th10; then [(y `1),(([y,x] `2) `1)] in the InternalRel of X ; then [(y `1),(x `1)] in the InternalRel of X ; then [y1,([x1,x2] `1)] in the InternalRel of X by A7, A10, MCART_1:7; then A12: [y1,x1] in the InternalRel of X ; [(([y,x] `1) `2),(([y,x] `2) `2)] in the InternalRel of Y by A11, Th10; then [(y `2),(([y,x] `2) `2)] in the InternalRel of Y ; then [(y `2),(x `2)] in the InternalRel of Y ; then [y2,([x1,x2] `2)] in the InternalRel of Y by A7, A10, MCART_1:7; then A13: [y2,x2] in the InternalRel of Y ; A14: [x,y] in [" the InternalRel of X, the InternalRel of Y"] by A3, Def2; then [(([x,y] `1) `2),(([x,y] `2) `2)] in the InternalRel of Y by Th10; then [(x `2),(([x,y] `2) `2)] in the InternalRel of Y ; then [(x `2),(y `2)] in the InternalRel of Y ; then [x2,([y1,y2] `2)] in the InternalRel of Y by A7, A10, MCART_1:7; then A15: [x2,y2] in the InternalRel of Y ; [(([x,y] `1) `1),(([x,y] `2) `1)] in the InternalRel of X by A14, Th10; then [(x `1),(([x,y] `2) `1)] in the InternalRel of X ; then [(x `1),(y `1)] in the InternalRel of X ; then [x1,([y1,y2] `1)] in the InternalRel of X by A7, A10, MCART_1:7; then [x1,y1] in the InternalRel of X ; then ( the InternalRel of Y is_antisymmetric_in the carrier of Y & x1 = y1 ) by A5, A8, A12, ORDERS_2:def_4, RELAT_2:def_4; hence x = y by A6, A7, A9, A10, A15, A13, RELAT_2:def_4; ::_thesis: verum end; end; registration let X, Y be transitive RelStr ; cluster[:X,Y:] -> strict transitive ; coherence [:X,Y:] is transitive proof set P = the InternalRel of X; set R = the InternalRel of Y; let x, y, z be set ; :: according to RELAT_2:def_8,ORDERS_2:def_3 ::_thesis: ( not x in the carrier of [:X,Y:] or not y in the carrier of [:X,Y:] or not z in the carrier of [:X,Y:] or not [x,y] in the InternalRel of [:X,Y:] or not [y,z] in the InternalRel of [:X,Y:] or [x,z] in the InternalRel of [:X,Y:] ) assume that A1: x in the carrier of [:X,Y:] and A2: y in the carrier of [:X,Y:] and A3: z in the carrier of [:X,Y:] and A4: [x,y] in the InternalRel of [:X,Y:] and A5: [y,z] in the InternalRel of [:X,Y:] ; ::_thesis: [x,z] in the InternalRel of [:X,Y:] y in [: the carrier of X, the carrier of Y:] by A2, Def2; then consider y1, y2 being set such that A6: y1 in the carrier of X and A7: y2 in the carrier of Y and A8: y = [y1,y2] by ZFMISC_1:def_2; z in [: the carrier of X, the carrier of Y:] by A3, Def2; then consider z1, z2 being set such that A9: z1 in the carrier of X and A10: z2 in the carrier of Y and A11: z = [z1,z2] by ZFMISC_1:def_2; A12: [y,z] in [" the InternalRel of X, the InternalRel of Y"] by A5, Def2; then [(([y,z] `1) `1),(([y,z] `2) `1)] in the InternalRel of X by Th10; then [(y `1),(([y,z] `2) `1)] in the InternalRel of X ; then [(y `1),(z `1)] in the InternalRel of X ; then [y1,(z `1)] in the InternalRel of X by A8, MCART_1:7; then A13: [y1,z1] in the InternalRel of X by A11, MCART_1:7; x in [: the carrier of X, the carrier of Y:] by A1, Def2; then consider x1, x2 being set such that A14: x1 in the carrier of X and A15: x2 in the carrier of Y and A16: x = [x1,x2] by ZFMISC_1:def_2; A17: [x,y] in [" the InternalRel of X, the InternalRel of Y"] by A4, Def2; then [(([x,y] `1) `1),(([x,y] `2) `1)] in the InternalRel of X by Th10; then [(x `1),(([x,y] `2) `1)] in the InternalRel of X ; then [(x `1),(y `1)] in the InternalRel of X ; then [x1,(y `1)] in the InternalRel of X by A16, MCART_1:7; then ( the InternalRel of X is_transitive_in the carrier of X & [x1,y1] in the InternalRel of X ) by A8, MCART_1:7, ORDERS_2:def_3; then [x1,z1] in the InternalRel of X by A14, A6, A9, A13, RELAT_2:def_8; then [x1,(z `1)] in the InternalRel of X by A11, MCART_1:7; then A18: [(x `1),(z `1)] in the InternalRel of X by A16, MCART_1:7; [(([y,z] `1) `2),(([y,z] `2) `2)] in the InternalRel of Y by A12, Th10; then [(y `2),(([y,z] `2) `2)] in the InternalRel of Y ; then [(y `2),(z `2)] in the InternalRel of Y ; then [y2,(z `2)] in the InternalRel of Y by A8, MCART_1:7; then A19: [y2,z2] in the InternalRel of Y by A11, MCART_1:7; [(([x,y] `1) `2),(([x,y] `2) `2)] in the InternalRel of Y by A17, Th10; then [(x `2),(([x,y] `2) `2)] in the InternalRel of Y ; then [(x `2),(y `2)] in the InternalRel of Y ; then [x2,(y `2)] in the InternalRel of Y by A16, MCART_1:7; then ( the InternalRel of Y is_transitive_in the carrier of Y & [x2,y2] in the InternalRel of Y ) by A8, MCART_1:7, ORDERS_2:def_3; then [x2,z2] in the InternalRel of Y by A15, A7, A10, A19, RELAT_2:def_8; then [x2,(z `2)] in the InternalRel of Y by A11, MCART_1:7; then A20: [(x `2),(z `2)] in the InternalRel of Y by A16, MCART_1:7; ( [x,z] `1 = x & [x,z] `2 = z ) ; then [x,z] in [" the InternalRel of X, the InternalRel of Y"] by A16, A11, A18, A20, Th10; hence [x,z] in the InternalRel of [:X,Y:] by Def2; ::_thesis: verum end; end; registration let X, Y be with_suprema RelStr ; cluster[:X,Y:] -> strict with_suprema ; coherence [:X,Y:] is with_suprema proof set IT = [:X,Y:]; let x, y be Element of [:X,Y:]; :: according to LATTICE3:def_10 ::_thesis: ex b1 being Element of the carrier of [:X,Y:] st ( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of [:X,Y:] holds ( not x <= b2 or not y <= b2 or b1 <= b2 ) ) ) consider zx being Element of X such that A1: ( x `1 <= zx & y `1 <= zx ) and A2: for z9 being Element of X st x `1 <= z9 & y `1 <= z9 holds zx <= z9 by LATTICE3:def_10; consider zy being Element of Y such that A3: ( x `2 <= zy & y `2 <= zy ) and A4: for z9 being Element of Y st x `2 <= z9 & y `2 <= z9 holds zy <= z9 by LATTICE3:def_10; A5: the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2; then A6: ( ex a, b being set st ( a in the carrier of X & b in the carrier of Y & x = [a,b] ) & ex c, d being set st ( c in the carrier of X & d in the carrier of Y & y = [c,d] ) ) by ZFMISC_1:def_2; take z = [zx,zy]; ::_thesis: ( x <= z & y <= z & ( for b1 being Element of the carrier of [:X,Y:] holds ( not x <= b1 or not y <= b1 or z <= b1 ) ) ) ( [(x `1),(x `2)] <= [zx,zy] & [(y `1),(y `2)] <= [zx,zy] ) by A1, A3, Th11; hence ( x <= z & y <= z ) by A6, MCART_1:8; ::_thesis: for b1 being Element of the carrier of [:X,Y:] holds ( not x <= b1 or not y <= b1 or z <= b1 ) let z9 be Element of [:X,Y:]; ::_thesis: ( not x <= z9 or not y <= z9 or z <= z9 ) A7: ex a, b being set st ( a in the carrier of X & b in the carrier of Y & z9 = [a,b] ) by A5, ZFMISC_1:def_2; assume A8: ( x <= z9 & y <= z9 ) ; ::_thesis: z <= z9 then ( x `2 <= z9 `2 & y `2 <= z9 `2 ) by Th12; then A9: zy <= z9 `2 by A4; ( x `1 <= z9 `1 & y `1 <= z9 `1 ) by A8, Th12; then zx <= z9 `1 by A2; then [zx,zy] <= [(z9 `1),(z9 `2)] by A9, Th11; hence z <= z9 by A7, MCART_1:8; ::_thesis: verum end; end; registration let X, Y be with_infima RelStr ; cluster[:X,Y:] -> strict with_infima ; coherence [:X,Y:] is with_infima proof set IT = [:X,Y:]; let x, y be Element of [:X,Y:]; :: according to LATTICE3:def_11 ::_thesis: ex b1 being Element of the carrier of [:X,Y:] st ( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of [:X,Y:] holds ( not b2 <= x or not b2 <= y or b2 <= b1 ) ) ) consider zx being Element of X such that A1: ( x `1 >= zx & y `1 >= zx ) and A2: for z9 being Element of X st x `1 >= z9 & y `1 >= z9 holds zx >= z9 by LATTICE3:def_11; consider zy being Element of Y such that A3: ( x `2 >= zy & y `2 >= zy ) and A4: for z9 being Element of Y st x `2 >= z9 & y `2 >= z9 holds zy >= z9 by LATTICE3:def_11; A5: the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2; then A6: ( ex a, b being set st ( a in the carrier of X & b in the carrier of Y & x = [a,b] ) & ex c, d being set st ( c in the carrier of X & d in the carrier of Y & y = [c,d] ) ) by ZFMISC_1:def_2; take z = [zx,zy]; ::_thesis: ( z <= x & z <= y & ( for b1 being Element of the carrier of [:X,Y:] holds ( not b1 <= x or not b1 <= y or b1 <= z ) ) ) ( [(x `1),(x `2)] >= [zx,zy] & [(y `1),(y `2)] >= [zx,zy] ) by A1, A3, Th11; hence ( x >= z & y >= z ) by A6, MCART_1:8; ::_thesis: for b1 being Element of the carrier of [:X,Y:] holds ( not b1 <= x or not b1 <= y or b1 <= z ) let z9 be Element of [:X,Y:]; ::_thesis: ( not z9 <= x or not z9 <= y or z9 <= z ) A7: ex a, b being set st ( a in the carrier of X & b in the carrier of Y & z9 = [a,b] ) by A5, ZFMISC_1:def_2; assume A8: ( x >= z9 & y >= z9 ) ; ::_thesis: z9 <= z then ( x `2 >= z9 `2 & y `2 >= z9 `2 ) by Th12; then A9: zy >= z9 `2 by A4; ( x `1 >= z9 `1 & y `1 >= z9 `1 ) by A8, Th12; then zx >= z9 `1 by A2; then [zx,zy] >= [(z9 `1),(z9 `2)] by A9, Th11; hence z9 <= z by A7, MCART_1:8; ::_thesis: verum end; end; theorem :: YELLOW_3:14 for X, Y being RelStr st not [:X,Y:] is empty holds ( not X is empty & not Y is empty ) proof let X, Y be RelStr ; ::_thesis: ( not [:X,Y:] is empty implies ( not X is empty & not Y is empty ) ) assume not [:X,Y:] is empty ; ::_thesis: ( not X is empty & not Y is empty ) then A1: ex x being set st x in the carrier of [:X,Y:] by XBOOLE_0:def_1; the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2; hence ( not X is empty & not Y is empty ) by A1, MCART_1:10; ::_thesis: verum end; theorem :: YELLOW_3:15 for X, Y being non empty RelStr st [:X,Y:] is reflexive holds ( X is reflexive & Y is reflexive ) proof let X, Y be non empty RelStr ; ::_thesis: ( [:X,Y:] is reflexive implies ( X is reflexive & Y is reflexive ) ) assume A1: [:X,Y:] is reflexive ; ::_thesis: ( X is reflexive & Y is reflexive ) for x being Element of X holds x <= x proof set y = the Element of Y; let x be Element of X; ::_thesis: x <= x [x, the Element of Y] <= [x, the Element of Y] by A1, YELLOW_0:def_1; hence x <= x by Th11; ::_thesis: verum end; hence X is reflexive by YELLOW_0:def_1; ::_thesis: Y is reflexive for y being Element of Y holds y <= y proof set x = the Element of X; let y be Element of Y; ::_thesis: y <= y [ the Element of X,y] <= [ the Element of X,y] by A1, YELLOW_0:def_1; hence y <= y by Th11; ::_thesis: verum end; hence Y is reflexive by YELLOW_0:def_1; ::_thesis: verum end; theorem :: YELLOW_3:16 for X, Y being non empty reflexive RelStr st [:X,Y:] is antisymmetric holds ( X is antisymmetric & Y is antisymmetric ) proof let X, Y be non empty reflexive RelStr ; ::_thesis: ( [:X,Y:] is antisymmetric implies ( X is antisymmetric & Y is antisymmetric ) ) assume A1: [:X,Y:] is antisymmetric ; ::_thesis: ( X is antisymmetric & Y is antisymmetric ) for x, y being Element of X st x <= y & y <= x holds x = y proof set z = the Element of Y; A2: the Element of Y <= the Element of Y ; let x, y be Element of X; ::_thesis: ( x <= y & y <= x implies x = y ) assume ( x <= y & y <= x ) ; ::_thesis: x = y then ( [x, the Element of Y] <= [y, the Element of Y] & [y, the Element of Y] <= [x, the Element of Y] ) by A2, Th11; then [x, the Element of Y] = [y, the Element of Y] by A1, YELLOW_0:def_3; hence x = y by XTUPLE_0:1; ::_thesis: verum end; hence X is antisymmetric by YELLOW_0:def_3; ::_thesis: Y is antisymmetric for x, y being Element of Y st x <= y & y <= x holds x = y proof set z = the Element of X; A3: the Element of X <= the Element of X ; let x, y be Element of Y; ::_thesis: ( x <= y & y <= x implies x = y ) assume ( x <= y & y <= x ) ; ::_thesis: x = y then ( [ the Element of X,x] <= [ the Element of X,y] & [ the Element of X,y] <= [ the Element of X,x] ) by A3, Th11; then [ the Element of X,x] = [ the Element of X,y] by A1, YELLOW_0:def_3; hence x = y by XTUPLE_0:1; ::_thesis: verum end; hence Y is antisymmetric by YELLOW_0:def_3; ::_thesis: verum end; theorem :: YELLOW_3:17 for X, Y being non empty reflexive RelStr st [:X,Y:] is transitive holds ( X is transitive & Y is transitive ) proof let X, Y be non empty reflexive RelStr ; ::_thesis: ( [:X,Y:] is transitive implies ( X is transitive & Y is transitive ) ) assume A1: [:X,Y:] is transitive ; ::_thesis: ( X is transitive & Y is transitive ) for x, y, z being Element of X st x <= y & y <= z holds x <= z proof set a = the Element of Y; A2: the Element of Y <= the Element of Y ; let x, y, z be Element of X; ::_thesis: ( x <= y & y <= z implies x <= z ) assume ( x <= y & y <= z ) ; ::_thesis: x <= z then ( [x, the Element of Y] <= [y, the Element of Y] & [y, the Element of Y] <= [z, the Element of Y] ) by A2, Th11; then [x, the Element of Y] <= [z, the Element of Y] by A1, YELLOW_0:def_2; hence x <= z by Th11; ::_thesis: verum end; hence X is transitive by YELLOW_0:def_2; ::_thesis: Y is transitive for x, y, z being Element of Y st x <= y & y <= z holds x <= z proof set a = the Element of X; A3: the Element of X <= the Element of X ; let x, y, z be Element of Y; ::_thesis: ( x <= y & y <= z implies x <= z ) assume ( x <= y & y <= z ) ; ::_thesis: x <= z then ( [ the Element of X,x] <= [ the Element of X,y] & [ the Element of X,y] <= [ the Element of X,z] ) by A3, Th11; then [ the Element of X,x] <= [ the Element of X,z] by A1, YELLOW_0:def_2; hence x <= z by Th11; ::_thesis: verum end; hence Y is transitive by YELLOW_0:def_2; ::_thesis: verum end; theorem :: YELLOW_3:18 for X, Y being non empty reflexive RelStr st [:X,Y:] is with_suprema holds ( X is with_suprema & Y is with_suprema ) proof let X, Y be non empty reflexive RelStr ; ::_thesis: ( [:X,Y:] is with_suprema implies ( X is with_suprema & Y is with_suprema ) ) assume A1: [:X,Y:] is with_suprema ; ::_thesis: ( X is with_suprema & Y is with_suprema ) A2: the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2; thus X is with_suprema ::_thesis: Y is with_suprema proof let x, y be Element of X; :: according to LATTICE3:def_10 ::_thesis: ex b1 being Element of the carrier of X st ( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of X holds ( not x <= b2 or not y <= b2 or b1 <= b2 ) ) ) set a = the Element of Y; A3: the Element of Y <= the Element of Y ; consider z being Element of [:X,Y:] such that A4: ( [x, the Element of Y] <= z & [y, the Element of Y] <= z ) and A5: for z9 being Element of [:X,Y:] st [x, the Element of Y] <= z9 & [y, the Element of Y] <= z9 holds z <= z9 by A1, LATTICE3:def_10; take z `1 ; ::_thesis: ( x <= z `1 & y <= z `1 & ( for b1 being Element of the carrier of X holds ( not x <= b1 or not y <= b1 or z `1 <= b1 ) ) ) A6: z = [(z `1),(z `2)] by A2, MCART_1:21; hence ( x <= z `1 & y <= z `1 ) by A4, Th11; ::_thesis: for b1 being Element of the carrier of X holds ( not x <= b1 or not y <= b1 or z `1 <= b1 ) let z9 be Element of X; ::_thesis: ( not x <= z9 or not y <= z9 or z `1 <= z9 ) assume ( x <= z9 & y <= z9 ) ; ::_thesis: z `1 <= z9 then ( [x, the Element of Y] <= [z9, the Element of Y] & [y, the Element of Y] <= [z9, the Element of Y] ) by A3, Th11; then z <= [z9, the Element of Y] by A5; hence z `1 <= z9 by A6, Th11; ::_thesis: verum end; set a = the Element of X; A7: the Element of X <= the Element of X ; let x, y be Element of Y; :: according to LATTICE3:def_10 ::_thesis: ex b1 being Element of the carrier of Y st ( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of Y holds ( not x <= b2 or not y <= b2 or b1 <= b2 ) ) ) consider z being Element of [:X,Y:] such that A8: ( [ the Element of X,x] <= z & [ the Element of X,y] <= z ) and A9: for z9 being Element of [:X,Y:] st [ the Element of X,x] <= z9 & [ the Element of X,y] <= z9 holds z <= z9 by A1, LATTICE3:def_10; take z `2 ; ::_thesis: ( x <= z `2 & y <= z `2 & ( for b1 being Element of the carrier of Y holds ( not x <= b1 or not y <= b1 or z `2 <= b1 ) ) ) A10: z = [(z `1),(z `2)] by A2, MCART_1:21; hence ( x <= z `2 & y <= z `2 ) by A8, Th11; ::_thesis: for b1 being Element of the carrier of Y holds ( not x <= b1 or not y <= b1 or z `2 <= b1 ) let z9 be Element of Y; ::_thesis: ( not x <= z9 or not y <= z9 or z `2 <= z9 ) assume ( x <= z9 & y <= z9 ) ; ::_thesis: z `2 <= z9 then ( [ the Element of X,x] <= [ the Element of X,z9] & [ the Element of X,y] <= [ the Element of X,z9] ) by A7, Th11; then z <= [ the Element of X,z9] by A9; hence z `2 <= z9 by A10, Th11; ::_thesis: verum end; theorem :: YELLOW_3:19 for X, Y being non empty reflexive RelStr st [:X,Y:] is with_infima holds ( X is with_infima & Y is with_infima ) proof let X, Y be non empty reflexive RelStr ; ::_thesis: ( [:X,Y:] is with_infima implies ( X is with_infima & Y is with_infima ) ) assume A1: [:X,Y:] is with_infima ; ::_thesis: ( X is with_infima & Y is with_infima ) A2: the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2; thus X is with_infima ::_thesis: Y is with_infima proof let x, y be Element of X; :: according to LATTICE3:def_11 ::_thesis: ex b1 being Element of the carrier of X st ( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of X holds ( not b2 <= x or not b2 <= y or b2 <= b1 ) ) ) set a = the Element of Y; A3: the Element of Y <= the Element of Y ; consider z being Element of [:X,Y:] such that A4: ( [x, the Element of Y] >= z & [y, the Element of Y] >= z ) and A5: for z9 being Element of [:X,Y:] st [x, the Element of Y] >= z9 & [y, the Element of Y] >= z9 holds z >= z9 by A1, LATTICE3:def_11; take z `1 ; ::_thesis: ( z `1 <= x & z `1 <= y & ( for b1 being Element of the carrier of X holds ( not b1 <= x or not b1 <= y or b1 <= z `1 ) ) ) A6: z = [(z `1),(z `2)] by A2, MCART_1:21; hence ( x >= z `1 & y >= z `1 ) by A4, Th11; ::_thesis: for b1 being Element of the carrier of X holds ( not b1 <= x or not b1 <= y or b1 <= z `1 ) let z9 be Element of X; ::_thesis: ( not z9 <= x or not z9 <= y or z9 <= z `1 ) assume ( x >= z9 & y >= z9 ) ; ::_thesis: z9 <= z `1 then ( [x, the Element of Y] >= [z9, the Element of Y] & [y, the Element of Y] >= [z9, the Element of Y] ) by A3, Th11; then z >= [z9, the Element of Y] by A5; hence z9 <= z `1 by A6, Th11; ::_thesis: verum end; set a = the Element of X; A7: the Element of X <= the Element of X ; let x, y be Element of Y; :: according to LATTICE3:def_11 ::_thesis: ex b1 being Element of the carrier of Y st ( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of Y holds ( not b2 <= x or not b2 <= y or b2 <= b1 ) ) ) consider z being Element of [:X,Y:] such that A8: ( [ the Element of X,x] >= z & [ the Element of X,y] >= z ) and A9: for z9 being Element of [:X,Y:] st [ the Element of X,x] >= z9 & [ the Element of X,y] >= z9 holds z >= z9 by A1, LATTICE3:def_11; take z `2 ; ::_thesis: ( z `2 <= x & z `2 <= y & ( for b1 being Element of the carrier of Y holds ( not b1 <= x or not b1 <= y or b1 <= z `2 ) ) ) A10: z = [(z `1),(z `2)] by A2, MCART_1:21; hence ( x >= z `2 & y >= z `2 ) by A8, Th11; ::_thesis: for b1 being Element of the carrier of Y holds ( not b1 <= x or not b1 <= y or b1 <= z `2 ) let z9 be Element of Y; ::_thesis: ( not z9 <= x or not z9 <= y or z9 <= z `2 ) assume ( x >= z9 & y >= z9 ) ; ::_thesis: z9 <= z `2 then ( [ the Element of X,x] >= [ the Element of X,z9] & [ the Element of X,y] >= [ the Element of X,z9] ) by A7, Th11; then z >= [ the Element of X,z9] by A9; hence z9 <= z `2 by A10, Th11; ::_thesis: verum end; definition let S1, S2 be RelStr ; let D1 be directed Subset of S1; let D2 be directed Subset of S2; :: original: [: redefine func[:D1,D2:] -> directed Subset of [:S1,S2:]; coherence [:D1,D2:] is directed Subset of [:S1,S2:] proof set X = [:D1,D2:]; [:D1,D2:] is directed proof let x, y be Element of [:S1,S2:]; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in [:D1,D2:] or not y in [:D1,D2:] or ex b1 being Element of the carrier of [:S1,S2:] st ( b1 in [:D1,D2:] & x <= b1 & y <= b1 ) ) assume that A1: x in [:D1,D2:] and A2: y in [:D1,D2:] ; ::_thesis: ex b1 being Element of the carrier of [:S1,S2:] st ( b1 in [:D1,D2:] & x <= b1 & y <= b1 ) consider x1, x2 being set such that A3: x1 in D1 and A4: x2 in D2 and A5: x = [x1,x2] by A1, ZFMISC_1:def_2; reconsider S29 = S2 as non empty RelStr by A4; reconsider S19 = S1 as non empty RelStr by A3; consider y1, y2 being set such that A6: y1 in D1 and A7: y2 in D2 and A8: y = [y1,y2] by A2, ZFMISC_1:def_2; reconsider x2 = x2, y2 = y2 as Element of S2 by A4, A7; consider xy2 being Element of S2 such that A9: xy2 in D2 and A10: ( x2 <= xy2 & y2 <= xy2 ) by A4, A7, WAYBEL_0:def_1; reconsider x1 = x1, y1 = y1 as Element of S1 by A3, A6; consider xy1 being Element of S1 such that A11: xy1 in D1 and A12: ( x1 <= xy1 & y1 <= xy1 ) by A3, A6, WAYBEL_0:def_1; reconsider xy29 = xy2 as Element of S29 ; reconsider xy19 = xy1 as Element of S19 ; [xy19,xy29] is Element of [:S19,S29:] ; then reconsider z = [xy1,xy2] as Element of [:S1,S2:] ; take z ; ::_thesis: ( z in [:D1,D2:] & x <= z & y <= z ) thus z in [:D1,D2:] by A11, A9, ZFMISC_1:87; ::_thesis: ( x <= z & y <= z ) ( not S1 is empty & not S2 is empty ) by A3, A4; hence ( x <= z & y <= z ) by A5, A8, A12, A10, Th11; ::_thesis: verum end; hence [:D1,D2:] is directed Subset of [:S1,S2:] ; ::_thesis: verum end; end; theorem :: YELLOW_3:20 for S1, S2 being non empty RelStr for D1 being non empty Subset of S1 for D2 being non empty Subset of S2 st [:D1,D2:] is directed holds ( D1 is directed & D2 is directed ) proof let S1, S2 be non empty RelStr ; ::_thesis: for D1 being non empty Subset of S1 for D2 being non empty Subset of S2 st [:D1,D2:] is directed holds ( D1 is directed & D2 is directed ) let D1 be non empty Subset of S1; ::_thesis: for D2 being non empty Subset of S2 st [:D1,D2:] is directed holds ( D1 is directed & D2 is directed ) let D2 be non empty Subset of S2; ::_thesis: ( [:D1,D2:] is directed implies ( D1 is directed & D2 is directed ) ) assume A1: [:D1,D2:] is directed ; ::_thesis: ( D1 is directed & D2 is directed ) thus D1 is directed ::_thesis: D2 is directed proof set q1 = the Element of D2; let x, y be Element of S1; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in D1 or not y in D1 or ex b1 being Element of the carrier of S1 st ( b1 in D1 & x <= b1 & y <= b1 ) ) assume ( x in D1 & y in D1 ) ; ::_thesis: ex b1 being Element of the carrier of S1 st ( b1 in D1 & x <= b1 & y <= b1 ) then ( [x, the Element of D2] in [:D1,D2:] & [y, the Element of D2] in [:D1,D2:] ) by ZFMISC_1:87; then consider z being Element of [:S1,S2:] such that A2: z in [:D1,D2:] and A3: ( [x, the Element of D2] <= z & [y, the Element of D2] <= z ) by A1, WAYBEL_0:def_1; reconsider z2 = z `2 as Element of D2 by A2, MCART_1:10; reconsider zz = z `1 as Element of D1 by A2, MCART_1:10; take zz ; ::_thesis: ( zz in D1 & x <= zz & y <= zz ) thus zz in D1 ; ::_thesis: ( x <= zz & y <= zz ) ex x, y being set st ( x in D1 & y in D2 & z = [x,y] ) by A2, ZFMISC_1:def_2; then ( [x, the Element of D2] <= [zz,z2] & [y, the Element of D2] <= [zz,z2] ) by A3, MCART_1:8; hence ( x <= zz & y <= zz ) by Th11; ::_thesis: verum end; set q1 = the Element of D1; let x, y be Element of S2; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in D2 or not y in D2 or ex b1 being Element of the carrier of S2 st ( b1 in D2 & x <= b1 & y <= b1 ) ) assume ( x in D2 & y in D2 ) ; ::_thesis: ex b1 being Element of the carrier of S2 st ( b1 in D2 & x <= b1 & y <= b1 ) then ( [ the Element of D1,x] in [:D1,D2:] & [ the Element of D1,y] in [:D1,D2:] ) by ZFMISC_1:87; then consider z being Element of [:S1,S2:] such that A4: z in [:D1,D2:] and A5: ( [ the Element of D1,x] <= z & [ the Element of D1,y] <= z ) by A1, WAYBEL_0:def_1; reconsider z2 = z `1 as Element of D1 by A4, MCART_1:10; reconsider zz = z `2 as Element of D2 by A4, MCART_1:10; take zz ; ::_thesis: ( zz in D2 & x <= zz & y <= zz ) thus zz in D2 ; ::_thesis: ( x <= zz & y <= zz ) ex x, y being set st ( x in D1 & y in D2 & z = [x,y] ) by A4, ZFMISC_1:def_2; then ( [ the Element of D1,x] <= [z2,zz] & [ the Element of D1,y] <= [z2,zz] ) by A5, MCART_1:8; hence ( x <= zz & y <= zz ) by Th11; ::_thesis: verum end; theorem Th21: :: YELLOW_3:21 for S1, S2 being non empty RelStr for D being non empty Subset of [:S1,S2:] holds ( not proj1 D is empty & not proj2 D is empty ) proof let S1, S2 be non empty RelStr ; ::_thesis: for D being non empty Subset of [:S1,S2:] holds ( not proj1 D is empty & not proj2 D is empty ) let D be non empty Subset of [:S1,S2:]; ::_thesis: ( not proj1 D is empty & not proj2 D is empty ) reconsider D1 = D as non empty Subset of [: the carrier of S1, the carrier of S2:] by Def2; not proj1 D1 is empty ; hence ( not proj1 D is empty & not proj2 D is empty ) ; ::_thesis: verum end; theorem :: YELLOW_3:22 for S1, S2 being non empty reflexive RelStr for D being non empty directed Subset of [:S1,S2:] holds ( proj1 D is directed & proj2 D is directed ) proof let S1, S2 be non empty reflexive RelStr ; ::_thesis: for D being non empty directed Subset of [:S1,S2:] holds ( proj1 D is directed & proj2 D is directed ) let D be non empty directed Subset of [:S1,S2:]; ::_thesis: ( proj1 D is directed & proj2 D is directed ) set D1 = proj1 D; set D2 = proj2 D; the carrier of [:S1,S2:] = [: the carrier of S1, the carrier of S2:] by Def2; then A1: D c= [:(proj1 D),(proj2 D):] by Th1; thus proj1 D is directed ::_thesis: proj2 D is directed proof let x, y be Element of S1; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in proj1 D or not y in proj1 D or ex b1 being Element of the carrier of S1 st ( b1 in proj1 D & x <= b1 & y <= b1 ) ) assume that A2: x in proj1 D and A3: y in proj1 D ; ::_thesis: ex b1 being Element of the carrier of S1 st ( b1 in proj1 D & x <= b1 & y <= b1 ) consider q2 being set such that A4: [y,q2] in D by A3, XTUPLE_0:def_12; reconsider D29 = proj2 D as non empty Subset of S2 by A2, FUNCT_5:16; reconsider D19 = proj1 D as non empty Subset of S1 by A2; consider q1 being set such that A5: [x,q1] in D by A2, XTUPLE_0:def_12; reconsider q2 = q2 as Element of D29 by A4, XTUPLE_0:def_13; reconsider q1 = q1 as Element of D29 by A5, XTUPLE_0:def_13; consider z being Element of [:S1,S2:] such that A6: z in D and A7: ( [x,q1] <= z & [y,q2] <= z ) by A5, A4, WAYBEL_0:def_1; reconsider z2 = z `2 as Element of D29 by A1, A6, MCART_1:10; reconsider zz = z `1 as Element of D19 by A1, A6, MCART_1:10; take zz ; ::_thesis: ( zz in proj1 D & x <= zz & y <= zz ) thus zz in proj1 D ; ::_thesis: ( x <= zz & y <= zz ) ex x, y being set st ( x in D19 & y in D29 & z = [x,y] ) by A1, A6, ZFMISC_1:def_2; then z = [zz,z2] by MCART_1:8; hence ( x <= zz & y <= zz ) by A7, Th11; ::_thesis: verum end; let x, y be Element of S2; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in proj2 D or not y in proj2 D or ex b1 being Element of the carrier of S2 st ( b1 in proj2 D & x <= b1 & y <= b1 ) ) assume that A8: x in proj2 D and A9: y in proj2 D ; ::_thesis: ex b1 being Element of the carrier of S2 st ( b1 in proj2 D & x <= b1 & y <= b1 ) consider q2 being set such that A10: [q2,y] in D by A9, XTUPLE_0:def_13; reconsider D29 = proj2 D as non empty Subset of S2 by A8; reconsider D19 = proj1 D as non empty Subset of S1 by A8, FUNCT_5:16; consider q1 being set such that A11: [q1,x] in D by A8, XTUPLE_0:def_13; reconsider q2 = q2 as Element of D19 by A10, XTUPLE_0:def_12; reconsider q1 = q1 as Element of D19 by A11, XTUPLE_0:def_12; consider z being Element of [:S1,S2:] such that A12: z in D and A13: ( [q1,x] <= z & [q2,y] <= z ) by A11, A10, WAYBEL_0:def_1; reconsider z2 = z `1 as Element of D19 by A1, A12, MCART_1:10; reconsider zz = z `2 as Element of D29 by A1, A12, MCART_1:10; take zz ; ::_thesis: ( zz in proj2 D & x <= zz & y <= zz ) thus zz in proj2 D ; ::_thesis: ( x <= zz & y <= zz ) ex x, y being set st ( x in D19 & y in D29 & z = [x,y] ) by A1, A12, ZFMISC_1:def_2; then z = [z2,zz] by MCART_1:8; hence ( x <= zz & y <= zz ) by A13, Th11; ::_thesis: verum end; definition let S1, S2 be RelStr ; let D1 be filtered Subset of S1; let D2 be filtered Subset of S2; :: original: [: redefine func[:D1,D2:] -> filtered Subset of [:S1,S2:]; coherence [:D1,D2:] is filtered Subset of [:S1,S2:] proof set X = [:D1,D2:]; [:D1,D2:] is filtered proof let x, y be Element of [:S1,S2:]; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in [:D1,D2:] or not y in [:D1,D2:] or ex b1 being Element of the carrier of [:S1,S2:] st ( b1 in [:D1,D2:] & b1 <= x & b1 <= y ) ) assume that A1: x in [:D1,D2:] and A2: y in [:D1,D2:] ; ::_thesis: ex b1 being Element of the carrier of [:S1,S2:] st ( b1 in [:D1,D2:] & b1 <= x & b1 <= y ) consider x1, x2 being set such that A3: x1 in D1 and A4: x2 in D2 and A5: x = [x1,x2] by A1, ZFMISC_1:def_2; reconsider S29 = S2 as non empty RelStr by A4; reconsider S19 = S1 as non empty RelStr by A3; consider y1, y2 being set such that A6: y1 in D1 and A7: y2 in D2 and A8: y = [y1,y2] by A2, ZFMISC_1:def_2; reconsider x2 = x2, y2 = y2 as Element of S2 by A4, A7; consider xy2 being Element of S2 such that A9: xy2 in D2 and A10: ( x2 >= xy2 & y2 >= xy2 ) by A4, A7, WAYBEL_0:def_2; reconsider x1 = x1, y1 = y1 as Element of S1 by A3, A6; consider xy1 being Element of S1 such that A11: xy1 in D1 and A12: ( x1 >= xy1 & y1 >= xy1 ) by A3, A6, WAYBEL_0:def_2; reconsider xy29 = xy2 as Element of S29 ; reconsider xy19 = xy1 as Element of S19 ; [xy19,xy29] is Element of [:S19,S29:] ; then reconsider z = [xy1,xy2] as Element of [:S1,S2:] ; take z ; ::_thesis: ( z in [:D1,D2:] & z <= x & z <= y ) thus z in [:D1,D2:] by A11, A9, ZFMISC_1:87; ::_thesis: ( z <= x & z <= y ) ( not S1 is empty & not S2 is empty ) by A3, A4; hence ( z <= x & z <= y ) by A5, A8, A12, A10, Th11; ::_thesis: verum end; hence [:D1,D2:] is filtered Subset of [:S1,S2:] ; ::_thesis: verum end; end; theorem :: YELLOW_3:23 for S1, S2 being non empty RelStr for D1 being non empty Subset of S1 for D2 being non empty Subset of S2 st [:D1,D2:] is filtered holds ( D1 is filtered & D2 is filtered ) proof let S1, S2 be non empty RelStr ; ::_thesis: for D1 being non empty Subset of S1 for D2 being non empty Subset of S2 st [:D1,D2:] is filtered holds ( D1 is filtered & D2 is filtered ) let D1 be non empty Subset of S1; ::_thesis: for D2 being non empty Subset of S2 st [:D1,D2:] is filtered holds ( D1 is filtered & D2 is filtered ) let D2 be non empty Subset of S2; ::_thesis: ( [:D1,D2:] is filtered implies ( D1 is filtered & D2 is filtered ) ) assume A1: [:D1,D2:] is filtered ; ::_thesis: ( D1 is filtered & D2 is filtered ) thus D1 is filtered ::_thesis: D2 is filtered proof set q1 = the Element of D2; let x, y be Element of S1; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in D1 or not y in D1 or ex b1 being Element of the carrier of S1 st ( b1 in D1 & b1 <= x & b1 <= y ) ) assume ( x in D1 & y in D1 ) ; ::_thesis: ex b1 being Element of the carrier of S1 st ( b1 in D1 & b1 <= x & b1 <= y ) then ( [x, the Element of D2] in [:D1,D2:] & [y, the Element of D2] in [:D1,D2:] ) by ZFMISC_1:87; then consider z being Element of [:S1,S2:] such that A2: z in [:D1,D2:] and A3: ( [x, the Element of D2] >= z & [y, the Element of D2] >= z ) by A1, WAYBEL_0:def_2; reconsider z2 = z `2 as Element of D2 by A2, MCART_1:10; reconsider zz = z `1 as Element of D1 by A2, MCART_1:10; take zz ; ::_thesis: ( zz in D1 & zz <= x & zz <= y ) thus zz in D1 ; ::_thesis: ( zz <= x & zz <= y ) ex x, y being set st ( x in D1 & y in D2 & z = [x,y] ) by A2, ZFMISC_1:def_2; then ( [x, the Element of D2] >= [zz,z2] & [y, the Element of D2] >= [zz,z2] ) by A3, MCART_1:8; hence ( zz <= x & zz <= y ) by Th11; ::_thesis: verum end; set q1 = the Element of D1; let x, y be Element of S2; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in D2 or not y in D2 or ex b1 being Element of the carrier of S2 st ( b1 in D2 & b1 <= x & b1 <= y ) ) assume ( x in D2 & y in D2 ) ; ::_thesis: ex b1 being Element of the carrier of S2 st ( b1 in D2 & b1 <= x & b1 <= y ) then ( [ the Element of D1,x] in [:D1,D2:] & [ the Element of D1,y] in [:D1,D2:] ) by ZFMISC_1:87; then consider z being Element of [:S1,S2:] such that A4: z in [:D1,D2:] and A5: ( [ the Element of D1,x] >= z & [ the Element of D1,y] >= z ) by A1, WAYBEL_0:def_2; reconsider z2 = z `1 as Element of D1 by A4, MCART_1:10; reconsider zz = z `2 as Element of D2 by A4, MCART_1:10; take zz ; ::_thesis: ( zz in D2 & zz <= x & zz <= y ) thus zz in D2 ; ::_thesis: ( zz <= x & zz <= y ) ex x, y being set st ( x in D1 & y in D2 & z = [x,y] ) by A4, ZFMISC_1:def_2; then ( [ the Element of D1,x] >= [z2,zz] & [ the Element of D1,y] >= [z2,zz] ) by A5, MCART_1:8; hence ( zz <= x & zz <= y ) by Th11; ::_thesis: verum end; theorem :: YELLOW_3:24 for S1, S2 being non empty reflexive RelStr for D being non empty filtered Subset of [:S1,S2:] holds ( proj1 D is filtered & proj2 D is filtered ) proof let S1, S2 be non empty reflexive RelStr ; ::_thesis: for D being non empty filtered Subset of [:S1,S2:] holds ( proj1 D is filtered & proj2 D is filtered ) let D be non empty filtered Subset of [:S1,S2:]; ::_thesis: ( proj1 D is filtered & proj2 D is filtered ) set D1 = proj1 D; set D2 = proj2 D; the carrier of [:S1,S2:] = [: the carrier of S1, the carrier of S2:] by Def2; then A1: D c= [:(proj1 D),(proj2 D):] by Th1; thus proj1 D is filtered ::_thesis: proj2 D is filtered proof let x, y be Element of S1; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in proj1 D or not y in proj1 D or ex b1 being Element of the carrier of S1 st ( b1 in proj1 D & b1 <= x & b1 <= y ) ) assume that A2: x in proj1 D and A3: y in proj1 D ; ::_thesis: ex b1 being Element of the carrier of S1 st ( b1 in proj1 D & b1 <= x & b1 <= y ) consider q2 being set such that A4: [y,q2] in D by A3, XTUPLE_0:def_12; reconsider D29 = proj2 D as non empty Subset of S2 by A2, FUNCT_5:16; reconsider D19 = proj1 D as non empty Subset of S1 by A2; consider q1 being set such that A5: [x,q1] in D by A2, XTUPLE_0:def_12; reconsider q2 = q2 as Element of D29 by A4, XTUPLE_0:def_13; reconsider q1 = q1 as Element of D29 by A5, XTUPLE_0:def_13; consider z being Element of [:S1,S2:] such that A6: z in D and A7: ( [x,q1] >= z & [y,q2] >= z ) by A5, A4, WAYBEL_0:def_2; reconsider z2 = z `2 as Element of D29 by A1, A6, MCART_1:10; reconsider zz = z `1 as Element of D19 by A1, A6, MCART_1:10; take zz ; ::_thesis: ( zz in proj1 D & zz <= x & zz <= y ) thus zz in proj1 D ; ::_thesis: ( zz <= x & zz <= y ) ex x, y being set st ( x in D19 & y in D29 & z = [x,y] ) by A1, A6, ZFMISC_1:def_2; then z = [zz,z2] by MCART_1:8; hence ( zz <= x & zz <= y ) by A7, Th11; ::_thesis: verum end; let x, y be Element of S2; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in proj2 D or not y in proj2 D or ex b1 being Element of the carrier of S2 st ( b1 in proj2 D & b1 <= x & b1 <= y ) ) assume that A8: x in proj2 D and A9: y in proj2 D ; ::_thesis: ex b1 being Element of the carrier of S2 st ( b1 in proj2 D & b1 <= x & b1 <= y ) consider q2 being set such that A10: [q2,y] in D by A9, XTUPLE_0:def_13; reconsider D29 = proj2 D as non empty Subset of S2 by A8; reconsider D19 = proj1 D as non empty Subset of S1 by A8, FUNCT_5:16; consider q1 being set such that A11: [q1,x] in D by A8, XTUPLE_0:def_13; reconsider q2 = q2 as Element of D19 by A10, XTUPLE_0:def_12; reconsider q1 = q1 as Element of D19 by A11, XTUPLE_0:def_12; consider z being Element of [:S1,S2:] such that A12: z in D and A13: ( [q1,x] >= z & [q2,y] >= z ) by A11, A10, WAYBEL_0:def_2; reconsider z2 = z `1 as Element of D19 by A1, A12, MCART_1:10; reconsider zz = z `2 as Element of D29 by A1, A12, MCART_1:10; take zz ; ::_thesis: ( zz in proj2 D & zz <= x & zz <= y ) thus zz in proj2 D ; ::_thesis: ( zz <= x & zz <= y ) ex x, y being set st ( x in D19 & y in D29 & z = [x,y] ) by A1, A12, ZFMISC_1:def_2; then z = [z2,zz] by MCART_1:8; hence ( zz <= x & zz <= y ) by A13, Th11; ::_thesis: verum end; definition let S1, S2 be RelStr ; let D1 be upper Subset of S1; let D2 be upper Subset of S2; :: original: [: redefine func[:D1,D2:] -> upper Subset of [:S1,S2:]; coherence [:D1,D2:] is upper Subset of [:S1,S2:] proof set X = [:D1,D2:]; [:D1,D2:] is upper proof let x, y be Element of [:S1,S2:]; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in [:D1,D2:] or not x <= y or y in [:D1,D2:] ) assume that A1: x in [:D1,D2:] and A2: x <= y ; ::_thesis: y in [:D1,D2:] consider x1, x2 being set such that A3: x1 in D1 and A4: x2 in D2 and A5: x = [x1,x2] by A1, ZFMISC_1:def_2; reconsider s1 = S1, s2 = S2 as non empty RelStr by A3, A4; set C1 = the carrier of s1; set C2 = the carrier of s2; the carrier of [:S1,S2:] = [: the carrier of s1, the carrier of s2:] by Def2; then consider y1, y2 being set such that A6: y1 in the carrier of s1 and A7: y2 in the carrier of s2 and A8: y = [y1,y2] by ZFMISC_1:def_2; reconsider x2 = x2, y2 = y2 as Element of s2 by A4, A7; x2 <= y2 by A2, A3, A5, A6, A8, Th11; then A9: y2 in D2 by A4, WAYBEL_0:def_20; reconsider x1 = x1, y1 = y1 as Element of s1 by A3, A6; x1 <= y1 by A2, A4, A5, A7, A8, Th11; then y1 in D1 by A3, WAYBEL_0:def_20; hence y in [:D1,D2:] by A8, A9, ZFMISC_1:87; ::_thesis: verum end; hence [:D1,D2:] is upper Subset of [:S1,S2:] ; ::_thesis: verum end; end; theorem :: YELLOW_3:25 for S1, S2 being non empty reflexive RelStr for D1 being non empty Subset of S1 for D2 being non empty Subset of S2 st [:D1,D2:] is upper holds ( D1 is upper & D2 is upper ) proof let S1, S2 be non empty reflexive RelStr ; ::_thesis: for D1 being non empty Subset of S1 for D2 being non empty Subset of S2 st [:D1,D2:] is upper holds ( D1 is upper & D2 is upper ) let D1 be non empty Subset of S1; ::_thesis: for D2 being non empty Subset of S2 st [:D1,D2:] is upper holds ( D1 is upper & D2 is upper ) let D2 be non empty Subset of S2; ::_thesis: ( [:D1,D2:] is upper implies ( D1 is upper & D2 is upper ) ) assume A1: [:D1,D2:] is upper ; ::_thesis: ( D1 is upper & D2 is upper ) thus D1 is upper ::_thesis: D2 is upper proof set q1 = the Element of D2; let x, y be Element of S1; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in D1 or not x <= y or y in D1 ) assume that A2: x in D1 and A3: x <= y ; ::_thesis: y in D1 A4: [x, the Element of D2] in [:D1,D2:] by A2, ZFMISC_1:87; the Element of D2 <= the Element of D2 ; then [x, the Element of D2] <= [y, the Element of D2] by A3, Th11; then [y, the Element of D2] in [:D1,D2:] by A1, A4, WAYBEL_0:def_20; hence y in D1 by ZFMISC_1:87; ::_thesis: verum end; set q1 = the Element of D1; let x, y be Element of S2; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in D2 or not x <= y or y in D2 ) assume that A5: x in D2 and A6: x <= y ; ::_thesis: y in D2 A7: [ the Element of D1,x] in [:D1,D2:] by A5, ZFMISC_1:87; the Element of D1 <= the Element of D1 ; then [ the Element of D1,x] <= [ the Element of D1,y] by A6, Th11; then [ the Element of D1,y] in [:D1,D2:] by A1, A7, WAYBEL_0:def_20; hence y in D2 by ZFMISC_1:87; ::_thesis: verum end; theorem :: YELLOW_3:26 for S1, S2 being non empty reflexive RelStr for D being non empty upper Subset of [:S1,S2:] holds ( proj1 D is upper & proj2 D is upper ) proof let S1, S2 be non empty reflexive RelStr ; ::_thesis: for D being non empty upper Subset of [:S1,S2:] holds ( proj1 D is upper & proj2 D is upper ) let D be non empty upper Subset of [:S1,S2:]; ::_thesis: ( proj1 D is upper & proj2 D is upper ) set D1 = proj1 D; set D2 = proj2 D; reconsider d1 = proj1 D as non empty Subset of S1 by Th21; the carrier of [:S1,S2:] = [: the carrier of S1, the carrier of S2:] by Def2; then A1: D c= [:(proj1 D),(proj2 D):] by Th1; thus proj1 D is upper ::_thesis: proj2 D is upper proof reconsider d2 = proj2 D as non empty Subset of S2 by Th21; let x, y be Element of S1; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in proj1 D or not x <= y or y in proj1 D ) assume that A2: x in proj1 D and A3: x <= y ; ::_thesis: y in proj1 D consider q1 being set such that A4: [x,q1] in D by A2, XTUPLE_0:def_12; reconsider q1 = q1 as Element of d2 by A1, A4, ZFMISC_1:87; q1 <= q1 ; then [x,q1] <= [y,q1] by A3, Th11; then [y,q1] in D by A4, WAYBEL_0:def_20; hence y in proj1 D by A1, ZFMISC_1:87; ::_thesis: verum end; let x, y be Element of S2; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in proj2 D or not x <= y or y in proj2 D ) assume that A5: x in proj2 D and A6: x <= y ; ::_thesis: y in proj2 D consider q1 being set such that A7: [q1,x] in D by A5, XTUPLE_0:def_13; reconsider q1 = q1 as Element of d1 by A1, A7, ZFMISC_1:87; q1 <= q1 ; then [q1,x] <= [q1,y] by A6, Th11; then [q1,y] in D by A7, WAYBEL_0:def_20; hence y in proj2 D by A1, ZFMISC_1:87; ::_thesis: verum end; definition let S1, S2 be RelStr ; let D1 be lower Subset of S1; let D2 be lower Subset of S2; :: original: [: redefine func[:D1,D2:] -> lower Subset of [:S1,S2:]; coherence [:D1,D2:] is lower Subset of [:S1,S2:] proof set X = [:D1,D2:]; [:D1,D2:] is lower proof let x, y be Element of [:S1,S2:]; :: according to WAYBEL_0:def_19 ::_thesis: ( not x in [:D1,D2:] or not y <= x or y in [:D1,D2:] ) assume that A1: x in [:D1,D2:] and A2: x >= y ; ::_thesis: y in [:D1,D2:] consider x1, x2 being set such that A3: x1 in D1 and A4: x2 in D2 and A5: x = [x1,x2] by A1, ZFMISC_1:def_2; reconsider s1 = S1, s2 = S2 as non empty RelStr by A3, A4; set C1 = the carrier of s1; set C2 = the carrier of s2; the carrier of [:S1,S2:] = [: the carrier of s1, the carrier of s2:] by Def2; then consider y1, y2 being set such that A6: y1 in the carrier of s1 and A7: y2 in the carrier of s2 and A8: y = [y1,y2] by ZFMISC_1:def_2; reconsider x2 = x2, y2 = y2 as Element of s2 by A4, A7; x2 >= y2 by A2, A3, A5, A6, A8, Th11; then A9: y2 in D2 by A4, WAYBEL_0:def_19; reconsider x1 = x1, y1 = y1 as Element of s1 by A3, A6; x1 >= y1 by A2, A4, A5, A7, A8, Th11; then y1 in D1 by A3, WAYBEL_0:def_19; hence y in [:D1,D2:] by A8, A9, ZFMISC_1:87; ::_thesis: verum end; hence [:D1,D2:] is lower Subset of [:S1,S2:] ; ::_thesis: verum end; end; theorem :: YELLOW_3:27 for S1, S2 being non empty reflexive RelStr for D1 being non empty Subset of S1 for D2 being non empty Subset of S2 st [:D1,D2:] is lower holds ( D1 is lower & D2 is lower ) proof let S1, S2 be non empty reflexive RelStr ; ::_thesis: for D1 being non empty Subset of S1 for D2 being non empty Subset of S2 st [:D1,D2:] is lower holds ( D1 is lower & D2 is lower ) let D1 be non empty Subset of S1; ::_thesis: for D2 being non empty Subset of S2 st [:D1,D2:] is lower holds ( D1 is lower & D2 is lower ) let D2 be non empty Subset of S2; ::_thesis: ( [:D1,D2:] is lower implies ( D1 is lower & D2 is lower ) ) assume A1: [:D1,D2:] is lower ; ::_thesis: ( D1 is lower & D2 is lower ) thus D1 is lower ::_thesis: D2 is lower proof set q1 = the Element of D2; let x, y be Element of S1; :: according to WAYBEL_0:def_19 ::_thesis: ( not x in D1 or not y <= x or y in D1 ) assume that A2: x in D1 and A3: x >= y ; ::_thesis: y in D1 A4: [x, the Element of D2] in [:D1,D2:] by A2, ZFMISC_1:87; the Element of D2 <= the Element of D2 ; then [x, the Element of D2] >= [y, the Element of D2] by A3, Th11; then [y, the Element of D2] in [:D1,D2:] by A1, A4, WAYBEL_0:def_19; hence y in D1 by ZFMISC_1:87; ::_thesis: verum end; set q1 = the Element of D1; let x, y be Element of S2; :: according to WAYBEL_0:def_19 ::_thesis: ( not x in D2 or not y <= x or y in D2 ) assume that A5: x in D2 and A6: x >= y ; ::_thesis: y in D2 A7: [ the Element of D1,x] in [:D1,D2:] by A5, ZFMISC_1:87; the Element of D1 <= the Element of D1 ; then [ the Element of D1,x] >= [ the Element of D1,y] by A6, Th11; then [ the Element of D1,y] in [:D1,D2:] by A1, A7, WAYBEL_0:def_19; hence y in D2 by ZFMISC_1:87; ::_thesis: verum end; theorem :: YELLOW_3:28 for S1, S2 being non empty reflexive RelStr for D being non empty lower Subset of [:S1,S2:] holds ( proj1 D is lower & proj2 D is lower ) proof let S1, S2 be non empty reflexive RelStr ; ::_thesis: for D being non empty lower Subset of [:S1,S2:] holds ( proj1 D is lower & proj2 D is lower ) let D be non empty lower Subset of [:S1,S2:]; ::_thesis: ( proj1 D is lower & proj2 D is lower ) set D1 = proj1 D; set D2 = proj2 D; reconsider d1 = proj1 D as non empty Subset of S1 by Th21; the carrier of [:S1,S2:] = [: the carrier of S1, the carrier of S2:] by Def2; then A1: D c= [:(proj1 D),(proj2 D):] by Th1; thus proj1 D is lower ::_thesis: proj2 D is lower proof reconsider d2 = proj2 D as non empty Subset of S2 by Th21; let x, y be Element of S1; :: according to WAYBEL_0:def_19 ::_thesis: ( not x in proj1 D or not y <= x or y in proj1 D ) assume that A2: x in proj1 D and A3: x >= y ; ::_thesis: y in proj1 D consider q1 being set such that A4: [x,q1] in D by A2, XTUPLE_0:def_12; reconsider q1 = q1 as Element of d2 by A1, A4, ZFMISC_1:87; q1 <= q1 ; then [x,q1] >= [y,q1] by A3, Th11; then [y,q1] in D by A4, WAYBEL_0:def_19; hence y in proj1 D by A1, ZFMISC_1:87; ::_thesis: verum end; let x, y be Element of S2; :: according to WAYBEL_0:def_19 ::_thesis: ( not x in proj2 D or not y <= x or y in proj2 D ) assume that A5: x in proj2 D and A6: x >= y ; ::_thesis: y in proj2 D consider q1 being set such that A7: [q1,x] in D by A5, XTUPLE_0:def_13; reconsider q1 = q1 as Element of d1 by A1, A7, ZFMISC_1:87; q1 <= q1 ; then [q1,x] >= [q1,y] by A6, Th11; then [q1,y] in D by A7, WAYBEL_0:def_19; hence y in proj2 D by A1, ZFMISC_1:87; ::_thesis: verum end; definition let R be RelStr ; attrR is void means :Def3: :: YELLOW_3:def 3 the InternalRel of R is empty ; end; :: deftheorem Def3 defines void YELLOW_3:def_3_:_ for R being RelStr holds ( R is void iff the InternalRel of R is empty ); registration cluster empty -> void for RelStr ; coherence for b1 being RelStr st b1 is empty holds b1 is void proof let R be RelStr ; ::_thesis: ( R is empty implies R is void ) assume R is empty ; ::_thesis: R is void then reconsider R1 = R as empty RelStr ; the InternalRel of R1 is empty ; hence the InternalRel of R is empty ; :: according to YELLOW_3:def_3 ::_thesis: verum end; end; registration cluster non empty strict V55() reflexive transitive antisymmetric non void for RelStr ; existence ex b1 being Poset st ( not b1 is void & not b1 is empty & b1 is strict ) proof set R = the non empty strict Poset; take the non empty strict Poset ; ::_thesis: ( not the non empty strict Poset is void & not the non empty strict Poset is empty & the non empty strict Poset is strict ) ( ex x being set st x in the carrier of the non empty strict Poset & the InternalRel of the non empty strict Poset is_reflexive_in the carrier of the non empty strict Poset ) by ORDERS_2:def_2, XBOOLE_0:def_1; hence not the InternalRel of the non empty strict Poset is empty by RELAT_2:def_1; :: according to YELLOW_3:def_3 ::_thesis: ( not the non empty strict Poset is empty & the non empty strict Poset is strict ) thus ( not the non empty strict Poset is empty & the non empty strict Poset is strict ) ; ::_thesis: verum end; end; registration cluster non void -> non empty for RelStr ; coherence for b1 being RelStr st not b1 is void holds not b1 is empty ; end; registration cluster non empty reflexive -> non void for RelStr ; coherence for b1 being RelStr st not b1 is empty & b1 is reflexive holds not b1 is void proof let R be RelStr ; ::_thesis: ( not R is empty & R is reflexive implies not R is void ) assume ( not R is empty & R is reflexive ) ; ::_thesis: not R is void then reconsider R1 = R as non empty reflexive RelStr ; ( ex x being set st x in the carrier of R1 & the InternalRel of R1 is_reflexive_in the carrier of R1 ) by ORDERS_2:def_2, XBOOLE_0:def_1; hence not the InternalRel of R is empty by RELAT_2:def_1; :: according to YELLOW_3:def_3 ::_thesis: verum end; end; registration let R be non void RelStr ; cluster the InternalRel of R -> non empty ; coherence not the InternalRel of R is empty by Def3; end; theorem Th29: :: YELLOW_3:29 for S1, S2 being non empty RelStr for D1 being non empty Subset of S1 for D2 being non empty Subset of S2 for x being Element of S1 for y being Element of S2 st [x,y] is_>=_than [:D1,D2:] holds ( x is_>=_than D1 & y is_>=_than D2 ) proof let S1, S2 be non empty RelStr ; ::_thesis: for D1 being non empty Subset of S1 for D2 being non empty Subset of S2 for x being Element of S1 for y being Element of S2 st [x,y] is_>=_than [:D1,D2:] holds ( x is_>=_than D1 & y is_>=_than D2 ) let D1 be non empty Subset of S1; ::_thesis: for D2 being non empty Subset of S2 for x being Element of S1 for y being Element of S2 st [x,y] is_>=_than [:D1,D2:] holds ( x is_>=_than D1 & y is_>=_than D2 ) let D2 be non empty Subset of S2; ::_thesis: for x being Element of S1 for y being Element of S2 st [x,y] is_>=_than [:D1,D2:] holds ( x is_>=_than D1 & y is_>=_than D2 ) let x be Element of S1; ::_thesis: for y being Element of S2 st [x,y] is_>=_than [:D1,D2:] holds ( x is_>=_than D1 & y is_>=_than D2 ) let y be Element of S2; ::_thesis: ( [x,y] is_>=_than [:D1,D2:] implies ( x is_>=_than D1 & y is_>=_than D2 ) ) assume A1: [x,y] is_>=_than [:D1,D2:] ; ::_thesis: ( x is_>=_than D1 & y is_>=_than D2 ) thus x is_>=_than D1 ::_thesis: y is_>=_than D2 proof set a = the Element of D2; let b be Element of S1; :: according to LATTICE3:def_9 ::_thesis: ( not b in D1 or b <= x ) assume b in D1 ; ::_thesis: b <= x then [b, the Element of D2] in [:D1,D2:] by ZFMISC_1:87; then [b, the Element of D2] <= [x,y] by A1, LATTICE3:def_9; hence b <= x by Th11; ::_thesis: verum end; set b = the Element of D1; let a be Element of S2; :: according to LATTICE3:def_9 ::_thesis: ( not a in D2 or a <= y ) assume a in D2 ; ::_thesis: a <= y then [ the Element of D1,a] in [:D1,D2:] by ZFMISC_1:87; then [ the Element of D1,a] <= [x,y] by A1, LATTICE3:def_9; hence a <= y by Th11; ::_thesis: verum end; theorem Th30: :: YELLOW_3:30 for S1, S2 being non empty RelStr for D1 being Subset of S1 for D2 being Subset of S2 for x being Element of S1 for y being Element of S2 st x is_>=_than D1 & y is_>=_than D2 holds [x,y] is_>=_than [:D1,D2:] proof let S1, S2 be non empty RelStr ; ::_thesis: for D1 being Subset of S1 for D2 being Subset of S2 for x being Element of S1 for y being Element of S2 st x is_>=_than D1 & y is_>=_than D2 holds [x,y] is_>=_than [:D1,D2:] let D1 be Subset of S1; ::_thesis: for D2 being Subset of S2 for x being Element of S1 for y being Element of S2 st x is_>=_than D1 & y is_>=_than D2 holds [x,y] is_>=_than [:D1,D2:] let D2 be Subset of S2; ::_thesis: for x being Element of S1 for y being Element of S2 st x is_>=_than D1 & y is_>=_than D2 holds [x,y] is_>=_than [:D1,D2:] let x be Element of S1; ::_thesis: for y being Element of S2 st x is_>=_than D1 & y is_>=_than D2 holds [x,y] is_>=_than [:D1,D2:] let y be Element of S2; ::_thesis: ( x is_>=_than D1 & y is_>=_than D2 implies [x,y] is_>=_than [:D1,D2:] ) assume A1: ( x is_>=_than D1 & y is_>=_than D2 ) ; ::_thesis: [x,y] is_>=_than [:D1,D2:] let b be Element of [:S1,S2:]; :: according to LATTICE3:def_9 ::_thesis: ( not b in [:D1,D2:] or b <= [x,y] ) assume b in [:D1,D2:] ; ::_thesis: b <= [x,y] then consider b1, b2 being set such that A2: b1 in D1 and A3: b2 in D2 and A4: b = [b1,b2] by ZFMISC_1:def_2; reconsider b2 = b2 as Element of S2 by A3; reconsider b1 = b1 as Element of S1 by A2; ( b1 <= x & b2 <= y ) by A1, A2, A3, LATTICE3:def_9; hence b <= [x,y] by A4, Th11; ::_thesis: verum end; theorem Th31: :: YELLOW_3:31 for S1, S2 being non empty RelStr for D being Subset of [:S1,S2:] for x being Element of S1 for y being Element of S2 holds ( [x,y] is_>=_than D iff ( x is_>=_than proj1 D & y is_>=_than proj2 D ) ) proof let S1, S2 be non empty RelStr ; ::_thesis: for D being Subset of [:S1,S2:] for x being Element of S1 for y being Element of S2 holds ( [x,y] is_>=_than D iff ( x is_>=_than proj1 D & y is_>=_than proj2 D ) ) let D be Subset of [:S1,S2:]; ::_thesis: for x being Element of S1 for y being Element of S2 holds ( [x,y] is_>=_than D iff ( x is_>=_than proj1 D & y is_>=_than proj2 D ) ) let x be Element of S1; ::_thesis: for y being Element of S2 holds ( [x,y] is_>=_than D iff ( x is_>=_than proj1 D & y is_>=_than proj2 D ) ) let y be Element of S2; ::_thesis: ( [x,y] is_>=_than D iff ( x is_>=_than proj1 D & y is_>=_than proj2 D ) ) set D1 = proj1 D; set D2 = proj2 D; hereby ::_thesis: ( x is_>=_than proj1 D & y is_>=_than proj2 D implies [x,y] is_>=_than D ) assume A1: [x,y] is_>=_than D ; ::_thesis: ( x is_>=_than proj1 D & y is_>=_than proj2 D ) thus x is_>=_than proj1 D ::_thesis: y is_>=_than proj2 D proof let q be Element of S1; :: according to LATTICE3:def_9 ::_thesis: ( not q in proj1 D or q <= x ) assume q in proj1 D ; ::_thesis: q <= x then consider z being set such that A2: [q,z] in D by XTUPLE_0:def_12; reconsider d2 = proj2 D as non empty Subset of S2 by A2, XTUPLE_0:def_13; reconsider z = z as Element of d2 by A2, XTUPLE_0:def_13; [x,y] >= [q,z] by A1, A2, LATTICE3:def_9; hence q <= x by Th11; ::_thesis: verum end; thus y is_>=_than proj2 D ::_thesis: verum proof let q be Element of S2; :: according to LATTICE3:def_9 ::_thesis: ( not q in proj2 D or q <= y ) assume q in proj2 D ; ::_thesis: q <= y then consider z being set such that A3: [z,q] in D by XTUPLE_0:def_13; reconsider d1 = proj1 D as non empty Subset of S1 by A3, XTUPLE_0:def_12; reconsider z = z as Element of d1 by A3, XTUPLE_0:def_12; [x,y] >= [z,q] by A1, A3, LATTICE3:def_9; hence q <= y by Th11; ::_thesis: verum end; end; assume ( x is_>=_than proj1 D & y is_>=_than proj2 D ) ; ::_thesis: [x,y] is_>=_than D then A4: [x,y] is_>=_than [:(proj1 D),(proj2 D):] by Th30; the carrier of [:S1,S2:] = [: the carrier of S1, the carrier of S2:] by Def2; then D c= [:(proj1 D),(proj2 D):] by Th1; hence [x,y] is_>=_than D by A4, YELLOW_0:9; ::_thesis: verum end; theorem Th32: :: YELLOW_3:32 for S1, S2 being non empty RelStr for D1 being non empty Subset of S1 for D2 being non empty Subset of S2 for x being Element of S1 for y being Element of S2 st [x,y] is_<=_than [:D1,D2:] holds ( x is_<=_than D1 & y is_<=_than D2 ) proof let S1, S2 be non empty RelStr ; ::_thesis: for D1 being non empty Subset of S1 for D2 being non empty Subset of S2 for x being Element of S1 for y being Element of S2 st [x,y] is_<=_than [:D1,D2:] holds ( x is_<=_than D1 & y is_<=_than D2 ) let D1 be non empty Subset of S1; ::_thesis: for D2 being non empty Subset of S2 for x being Element of S1 for y being Element of S2 st [x,y] is_<=_than [:D1,D2:] holds ( x is_<=_than D1 & y is_<=_than D2 ) let D2 be non empty Subset of S2; ::_thesis: for x being Element of S1 for y being Element of S2 st [x,y] is_<=_than [:D1,D2:] holds ( x is_<=_than D1 & y is_<=_than D2 ) let x be Element of S1; ::_thesis: for y being Element of S2 st [x,y] is_<=_than [:D1,D2:] holds ( x is_<=_than D1 & y is_<=_than D2 ) let y be Element of S2; ::_thesis: ( [x,y] is_<=_than [:D1,D2:] implies ( x is_<=_than D1 & y is_<=_than D2 ) ) assume A1: [x,y] is_<=_than [:D1,D2:] ; ::_thesis: ( x is_<=_than D1 & y is_<=_than D2 ) thus x is_<=_than D1 ::_thesis: y is_<=_than D2 proof set a = the Element of D2; let b be Element of S1; :: according to LATTICE3:def_8 ::_thesis: ( not b in D1 or x <= b ) assume b in D1 ; ::_thesis: x <= b then [b, the Element of D2] in [:D1,D2:] by ZFMISC_1:87; then [b, the Element of D2] >= [x,y] by A1, LATTICE3:def_8; hence x <= b by Th11; ::_thesis: verum end; set b = the Element of D1; let a be Element of S2; :: according to LATTICE3:def_8 ::_thesis: ( not a in D2 or y <= a ) assume a in D2 ; ::_thesis: y <= a then [ the Element of D1,a] in [:D1,D2:] by ZFMISC_1:87; then [ the Element of D1,a] >= [x,y] by A1, LATTICE3:def_8; hence y <= a by Th11; ::_thesis: verum end; theorem Th33: :: YELLOW_3:33 for S1, S2 being non empty RelStr for D1 being Subset of S1 for D2 being Subset of S2 for x being Element of S1 for y being Element of S2 st x is_<=_than D1 & y is_<=_than D2 holds [x,y] is_<=_than [:D1,D2:] proof let S1, S2 be non empty RelStr ; ::_thesis: for D1 being Subset of S1 for D2 being Subset of S2 for x being Element of S1 for y being Element of S2 st x is_<=_than D1 & y is_<=_than D2 holds [x,y] is_<=_than [:D1,D2:] let D1 be Subset of S1; ::_thesis: for D2 being Subset of S2 for x being Element of S1 for y being Element of S2 st x is_<=_than D1 & y is_<=_than D2 holds [x,y] is_<=_than [:D1,D2:] let D2 be Subset of S2; ::_thesis: for x being Element of S1 for y being Element of S2 st x is_<=_than D1 & y is_<=_than D2 holds [x,y] is_<=_than [:D1,D2:] let x be Element of S1; ::_thesis: for y being Element of S2 st x is_<=_than D1 & y is_<=_than D2 holds [x,y] is_<=_than [:D1,D2:] let y be Element of S2; ::_thesis: ( x is_<=_than D1 & y is_<=_than D2 implies [x,y] is_<=_than [:D1,D2:] ) assume A1: ( x is_<=_than D1 & y is_<=_than D2 ) ; ::_thesis: [x,y] is_<=_than [:D1,D2:] let b be Element of [:S1,S2:]; :: according to LATTICE3:def_8 ::_thesis: ( not b in [:D1,D2:] or [x,y] <= b ) assume b in [:D1,D2:] ; ::_thesis: [x,y] <= b then consider b1, b2 being set such that A2: b1 in D1 and A3: b2 in D2 and A4: b = [b1,b2] by ZFMISC_1:def_2; reconsider b2 = b2 as Element of S2 by A3; reconsider b1 = b1 as Element of S1 by A2; ( b1 >= x & b2 >= y ) by A1, A2, A3, LATTICE3:def_8; hence [x,y] <= b by A4, Th11; ::_thesis: verum end; theorem Th34: :: YELLOW_3:34 for S1, S2 being non empty RelStr for D being Subset of [:S1,S2:] for x being Element of S1 for y being Element of S2 holds ( [x,y] is_<=_than D iff ( x is_<=_than proj1 D & y is_<=_than proj2 D ) ) proof let S1, S2 be non empty RelStr ; ::_thesis: for D being Subset of [:S1,S2:] for x being Element of S1 for y being Element of S2 holds ( [x,y] is_<=_than D iff ( x is_<=_than proj1 D & y is_<=_than proj2 D ) ) let D be Subset of [:S1,S2:]; ::_thesis: for x being Element of S1 for y being Element of S2 holds ( [x,y] is_<=_than D iff ( x is_<=_than proj1 D & y is_<=_than proj2 D ) ) let x be Element of S1; ::_thesis: for y being Element of S2 holds ( [x,y] is_<=_than D iff ( x is_<=_than proj1 D & y is_<=_than proj2 D ) ) let y be Element of S2; ::_thesis: ( [x,y] is_<=_than D iff ( x is_<=_than proj1 D & y is_<=_than proj2 D ) ) set D1 = proj1 D; set D2 = proj2 D; hereby ::_thesis: ( x is_<=_than proj1 D & y is_<=_than proj2 D implies [x,y] is_<=_than D ) assume A1: [x,y] is_<=_than D ; ::_thesis: ( x is_<=_than proj1 D & y is_<=_than proj2 D ) thus x is_<=_than proj1 D ::_thesis: y is_<=_than proj2 D proof let q be Element of S1; :: according to LATTICE3:def_8 ::_thesis: ( not q in proj1 D or x <= q ) assume q in proj1 D ; ::_thesis: x <= q then consider z being set such that A2: [q,z] in D by XTUPLE_0:def_12; reconsider d2 = proj2 D as non empty Subset of S2 by A2, XTUPLE_0:def_13; reconsider z = z as Element of d2 by A2, XTUPLE_0:def_13; [x,y] <= [q,z] by A1, A2, LATTICE3:def_8; hence x <= q by Th11; ::_thesis: verum end; thus y is_<=_than proj2 D ::_thesis: verum proof let q be Element of S2; :: according to LATTICE3:def_8 ::_thesis: ( not q in proj2 D or y <= q ) assume q in proj2 D ; ::_thesis: y <= q then consider z being set such that A3: [z,q] in D by XTUPLE_0:def_13; reconsider d1 = proj1 D as non empty Subset of S1 by A3, XTUPLE_0:def_12; reconsider z = z as Element of d1 by A3, XTUPLE_0:def_12; [x,y] <= [z,q] by A1, A3, LATTICE3:def_8; hence y <= q by Th11; ::_thesis: verum end; end; assume ( x is_<=_than proj1 D & y is_<=_than proj2 D ) ; ::_thesis: [x,y] is_<=_than D then A4: [x,y] is_<=_than [:(proj1 D),(proj2 D):] by Th33; the carrier of [:S1,S2:] = [: the carrier of S1, the carrier of S2:] by Def2; then D c= [:(proj1 D),(proj2 D):] by Th1; hence [x,y] is_<=_than D by A4, YELLOW_0:9; ::_thesis: verum end; theorem Th35: :: YELLOW_3:35 for S1, S2 being non empty antisymmetric RelStr for D1 being Subset of S1 for D2 being Subset of S2 for x being Element of S1 for y being Element of S2 st ex_sup_of D1,S1 & ex_sup_of D2,S2 & ( for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds [x,y] <= b ) holds ( ( for c being Element of S1 st c is_>=_than D1 holds x <= c ) & ( for d being Element of S2 st d is_>=_than D2 holds y <= d ) ) proof let S1, S2 be non empty antisymmetric RelStr ; ::_thesis: for D1 being Subset of S1 for D2 being Subset of S2 for x being Element of S1 for y being Element of S2 st ex_sup_of D1,S1 & ex_sup_of D2,S2 & ( for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds [x,y] <= b ) holds ( ( for c being Element of S1 st c is_>=_than D1 holds x <= c ) & ( for d being Element of S2 st d is_>=_than D2 holds y <= d ) ) let D1 be Subset of S1; ::_thesis: for D2 being Subset of S2 for x being Element of S1 for y being Element of S2 st ex_sup_of D1,S1 & ex_sup_of D2,S2 & ( for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds [x,y] <= b ) holds ( ( for c being Element of S1 st c is_>=_than D1 holds x <= c ) & ( for d being Element of S2 st d is_>=_than D2 holds y <= d ) ) let D2 be Subset of S2; ::_thesis: for x being Element of S1 for y being Element of S2 st ex_sup_of D1,S1 & ex_sup_of D2,S2 & ( for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds [x,y] <= b ) holds ( ( for c being Element of S1 st c is_>=_than D1 holds x <= c ) & ( for d being Element of S2 st d is_>=_than D2 holds y <= d ) ) let x be Element of S1; ::_thesis: for y being Element of S2 st ex_sup_of D1,S1 & ex_sup_of D2,S2 & ( for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds [x,y] <= b ) holds ( ( for c being Element of S1 st c is_>=_than D1 holds x <= c ) & ( for d being Element of S2 st d is_>=_than D2 holds y <= d ) ) let y be Element of S2; ::_thesis: ( ex_sup_of D1,S1 & ex_sup_of D2,S2 & ( for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds [x,y] <= b ) implies ( ( for c being Element of S1 st c is_>=_than D1 holds x <= c ) & ( for d being Element of S2 st d is_>=_than D2 holds y <= d ) ) ) assume that A1: ex_sup_of D1,S1 and A2: ex_sup_of D2,S2 and A3: for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds [x,y] <= b ; ::_thesis: ( ( for c being Element of S1 st c is_>=_than D1 holds x <= c ) & ( for d being Element of S2 st d is_>=_than D2 holds y <= d ) ) thus for c being Element of S1 st c is_>=_than D1 holds x <= c ::_thesis: for d being Element of S2 st d is_>=_than D2 holds y <= d proof A4: sup D2 is_>=_than D2 by A2, YELLOW_0:30; let b be Element of S1; ::_thesis: ( b is_>=_than D1 implies x <= b ) assume b is_>=_than D1 ; ::_thesis: x <= b then [x,y] <= [b,(sup D2)] by A3, A4, Th30; hence x <= b by Th11; ::_thesis: verum end; A5: sup D1 is_>=_than D1 by A1, YELLOW_0:30; let b be Element of S2; ::_thesis: ( b is_>=_than D2 implies y <= b ) assume b is_>=_than D2 ; ::_thesis: y <= b then [x,y] <= [(sup D1),b] by A3, A5, Th30; hence y <= b by Th11; ::_thesis: verum end; theorem Th36: :: YELLOW_3:36 for S1, S2 being non empty antisymmetric RelStr for D1 being Subset of S1 for D2 being Subset of S2 for x being Element of S1 for y being Element of S2 st ex_inf_of D1,S1 & ex_inf_of D2,S2 & ( for b being Element of [:S1,S2:] st b is_<=_than [:D1,D2:] holds [x,y] >= b ) holds ( ( for c being Element of S1 st c is_<=_than D1 holds x >= c ) & ( for d being Element of S2 st d is_<=_than D2 holds y >= d ) ) proof let S1, S2 be non empty antisymmetric RelStr ; ::_thesis: for D1 being Subset of S1 for D2 being Subset of S2 for x being Element of S1 for y being Element of S2 st ex_inf_of D1,S1 & ex_inf_of D2,S2 & ( for b being Element of [:S1,S2:] st b is_<=_than [:D1,D2:] holds [x,y] >= b ) holds ( ( for c being Element of S1 st c is_<=_than D1 holds x >= c ) & ( for d being Element of S2 st d is_<=_than D2 holds y >= d ) ) let D1 be Subset of S1; ::_thesis: for D2 being Subset of S2 for x being Element of S1 for y being Element of S2 st ex_inf_of D1,S1 & ex_inf_of D2,S2 & ( for b being Element of [:S1,S2:] st b is_<=_than [:D1,D2:] holds [x,y] >= b ) holds ( ( for c being Element of S1 st c is_<=_than D1 holds x >= c ) & ( for d being Element of S2 st d is_<=_than D2 holds y >= d ) ) let D2 be Subset of S2; ::_thesis: for x being Element of S1 for y being Element of S2 st ex_inf_of D1,S1 & ex_inf_of D2,S2 & ( for b being Element of [:S1,S2:] st b is_<=_than [:D1,D2:] holds [x,y] >= b ) holds ( ( for c being Element of S1 st c is_<=_than D1 holds x >= c ) & ( for d being Element of S2 st d is_<=_than D2 holds y >= d ) ) let x be Element of S1; ::_thesis: for y being Element of S2 st ex_inf_of D1,S1 & ex_inf_of D2,S2 & ( for b being Element of [:S1,S2:] st b is_<=_than [:D1,D2:] holds [x,y] >= b ) holds ( ( for c being Element of S1 st c is_<=_than D1 holds x >= c ) & ( for d being Element of S2 st d is_<=_than D2 holds y >= d ) ) let y be Element of S2; ::_thesis: ( ex_inf_of D1,S1 & ex_inf_of D2,S2 & ( for b being Element of [:S1,S2:] st b is_<=_than [:D1,D2:] holds [x,y] >= b ) implies ( ( for c being Element of S1 st c is_<=_than D1 holds x >= c ) & ( for d being Element of S2 st d is_<=_than D2 holds y >= d ) ) ) assume that A1: ex_inf_of D1,S1 and A2: ex_inf_of D2,S2 and A3: for b being Element of [:S1,S2:] st b is_<=_than [:D1,D2:] holds [x,y] >= b ; ::_thesis: ( ( for c being Element of S1 st c is_<=_than D1 holds x >= c ) & ( for d being Element of S2 st d is_<=_than D2 holds y >= d ) ) thus for c being Element of S1 st c is_<=_than D1 holds x >= c ::_thesis: for d being Element of S2 st d is_<=_than D2 holds y >= d proof A4: inf D2 is_<=_than D2 by A2, YELLOW_0:31; let b be Element of S1; ::_thesis: ( b is_<=_than D1 implies x >= b ) assume b is_<=_than D1 ; ::_thesis: x >= b then [x,y] >= [b,(inf D2)] by A3, A4, Th33; hence x >= b by Th11; ::_thesis: verum end; A5: inf D1 is_<=_than D1 by A1, YELLOW_0:31; let b be Element of S2; ::_thesis: ( b is_<=_than D2 implies y >= b ) assume b is_<=_than D2 ; ::_thesis: y >= b then [x,y] >= [(inf D1),b] by A3, A5, Th33; hence y >= b by Th11; ::_thesis: verum end; theorem :: YELLOW_3:37 for S1, S2 being non empty antisymmetric RelStr for D1 being non empty Subset of S1 for D2 being non empty Subset of S2 for x being Element of S1 for y being Element of S2 st ( for c being Element of S1 st c is_>=_than D1 holds x <= c ) & ( for d being Element of S2 st d is_>=_than D2 holds y <= d ) holds for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds [x,y] <= b proof let S1, S2 be non empty antisymmetric RelStr ; ::_thesis: for D1 being non empty Subset of S1 for D2 being non empty Subset of S2 for x being Element of S1 for y being Element of S2 st ( for c being Element of S1 st c is_>=_than D1 holds x <= c ) & ( for d being Element of S2 st d is_>=_than D2 holds y <= d ) holds for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds [x,y] <= b let D1 be non empty Subset of S1; ::_thesis: for D2 being non empty Subset of S2 for x being Element of S1 for y being Element of S2 st ( for c being Element of S1 st c is_>=_than D1 holds x <= c ) & ( for d being Element of S2 st d is_>=_than D2 holds y <= d ) holds for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds [x,y] <= b let D2 be non empty Subset of S2; ::_thesis: for x being Element of S1 for y being Element of S2 st ( for c being Element of S1 st c is_>=_than D1 holds x <= c ) & ( for d being Element of S2 st d is_>=_than D2 holds y <= d ) holds for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds [x,y] <= b let x be Element of S1; ::_thesis: for y being Element of S2 st ( for c being Element of S1 st c is_>=_than D1 holds x <= c ) & ( for d being Element of S2 st d is_>=_than D2 holds y <= d ) holds for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds [x,y] <= b let y be Element of S2; ::_thesis: ( ( for c being Element of S1 st c is_>=_than D1 holds x <= c ) & ( for d being Element of S2 st d is_>=_than D2 holds y <= d ) implies for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds [x,y] <= b ) assume that A1: for c being Element of S1 st c is_>=_than D1 holds x <= c and A2: for d being Element of S2 st d is_>=_than D2 holds y <= d ; ::_thesis: for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds [x,y] <= b let b be Element of [:S1,S2:]; ::_thesis: ( b is_>=_than [:D1,D2:] implies [x,y] <= b ) assume A3: b is_>=_than [:D1,D2:] ; ::_thesis: [x,y] <= b the carrier of [:S1,S2:] = [: the carrier of S1, the carrier of S2:] by Def2; then ex c, d being set st ( c in the carrier of S1 & d in the carrier of S2 & b = [c,d] ) by ZFMISC_1:def_2; then A4: b = [(b `1),(b `2)] by MCART_1:8; then b `2 is_>=_than D2 by A3, Th29; then A5: y <= b `2 by A2; b `1 is_>=_than D1 by A3, A4, Th29; then x <= b `1 by A1; hence [x,y] <= b by A4, A5, Th11; ::_thesis: verum end; theorem :: YELLOW_3:38 for S1, S2 being non empty antisymmetric RelStr for D1 being non empty Subset of S1 for D2 being non empty Subset of S2 for x being Element of S1 for y being Element of S2 st ( for c being Element of S1 st c is_>=_than D1 holds x >= c ) & ( for d being Element of S2 st d is_>=_than D2 holds y >= d ) holds for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds [x,y] >= b proof let S1, S2 be non empty antisymmetric RelStr ; ::_thesis: for D1 being non empty Subset of S1 for D2 being non empty Subset of S2 for x being Element of S1 for y being Element of S2 st ( for c being Element of S1 st c is_>=_than D1 holds x >= c ) & ( for d being Element of S2 st d is_>=_than D2 holds y >= d ) holds for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds [x,y] >= b let D1 be non empty Subset of S1; ::_thesis: for D2 being non empty Subset of S2 for x being Element of S1 for y being Element of S2 st ( for c being Element of S1 st c is_>=_than D1 holds x >= c ) & ( for d being Element of S2 st d is_>=_than D2 holds y >= d ) holds for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds [x,y] >= b let D2 be non empty Subset of S2; ::_thesis: for x being Element of S1 for y being Element of S2 st ( for c being Element of S1 st c is_>=_than D1 holds x >= c ) & ( for d being Element of S2 st d is_>=_than D2 holds y >= d ) holds for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds [x,y] >= b let x be Element of S1; ::_thesis: for y being Element of S2 st ( for c being Element of S1 st c is_>=_than D1 holds x >= c ) & ( for d being Element of S2 st d is_>=_than D2 holds y >= d ) holds for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds [x,y] >= b let y be Element of S2; ::_thesis: ( ( for c being Element of S1 st c is_>=_than D1 holds x >= c ) & ( for d being Element of S2 st d is_>=_than D2 holds y >= d ) implies for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds [x,y] >= b ) assume that A1: for c being Element of S1 st c is_>=_than D1 holds x >= c and A2: for d being Element of S2 st d is_>=_than D2 holds y >= d ; ::_thesis: for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds [x,y] >= b let b be Element of [:S1,S2:]; ::_thesis: ( b is_>=_than [:D1,D2:] implies [x,y] >= b ) assume A3: b is_>=_than [:D1,D2:] ; ::_thesis: [x,y] >= b the carrier of [:S1,S2:] = [: the carrier of S1, the carrier of S2:] by Def2; then ex c, d being set st ( c in the carrier of S1 & d in the carrier of S2 & b = [c,d] ) by ZFMISC_1:def_2; then A4: b = [(b `1),(b `2)] by MCART_1:8; then b `2 is_>=_than D2 by A3, Th29; then A5: y >= b `2 by A2; b `1 is_>=_than D1 by A3, A4, Th29; then x >= b `1 by A1; hence [x,y] >= b by A4, A5, Th11; ::_thesis: verum end; theorem Th39: :: YELLOW_3:39 for S1, S2 being non empty antisymmetric RelStr for D1 being non empty Subset of S1 for D2 being non empty Subset of S2 holds ( ( ex_sup_of D1,S1 & ex_sup_of D2,S2 ) iff ex_sup_of [:D1,D2:],[:S1,S2:] ) proof let S1, S2 be non empty antisymmetric RelStr ; ::_thesis: for D1 being non empty Subset of S1 for D2 being non empty Subset of S2 holds ( ( ex_sup_of D1,S1 & ex_sup_of D2,S2 ) iff ex_sup_of [:D1,D2:],[:S1,S2:] ) let D1 be non empty Subset of S1; ::_thesis: for D2 being non empty Subset of S2 holds ( ( ex_sup_of D1,S1 & ex_sup_of D2,S2 ) iff ex_sup_of [:D1,D2:],[:S1,S2:] ) let D2 be non empty Subset of S2; ::_thesis: ( ( ex_sup_of D1,S1 & ex_sup_of D2,S2 ) iff ex_sup_of [:D1,D2:],[:S1,S2:] ) hereby ::_thesis: ( ex_sup_of [:D1,D2:],[:S1,S2:] implies ( ex_sup_of D1,S1 & ex_sup_of D2,S2 ) ) assume that A1: ex_sup_of D1,S1 and A2: ex_sup_of D2,S2 ; ::_thesis: ex_sup_of [:D1,D2:],[:S1,S2:] consider a2 being Element of S2 such that A3: D2 is_<=_than a2 and A4: for b being Element of S2 st D2 is_<=_than b holds a2 <= b by A2, YELLOW_0:15; consider a1 being Element of S1 such that A5: D1 is_<=_than a1 and A6: for b being Element of S1 st D1 is_<=_than b holds a1 <= b by A1, YELLOW_0:15; ex a being Element of [:S1,S2:] st ( [:D1,D2:] is_<=_than a & ( for b being Element of [:S1,S2:] st [:D1,D2:] is_<=_than b holds a <= b ) ) proof take a = [a1,a2]; ::_thesis: ( [:D1,D2:] is_<=_than a & ( for b being Element of [:S1,S2:] st [:D1,D2:] is_<=_than b holds a <= b ) ) thus [:D1,D2:] is_<=_than a by A5, A3, Th30; ::_thesis: for b being Element of [:S1,S2:] st [:D1,D2:] is_<=_than b holds a <= b let b be Element of [:S1,S2:]; ::_thesis: ( [:D1,D2:] is_<=_than b implies a <= b ) assume A7: [:D1,D2:] is_<=_than b ; ::_thesis: a <= b the carrier of [:S1,S2:] = [: the carrier of S1, the carrier of S2:] by Def2; then A8: b = [(b `1),(b `2)] by MCART_1:21; then D2 is_<=_than b `2 by A7, Th29; then A9: a2 <= b `2 by A4; D1 is_<=_than b `1 by A7, A8, Th29; then a1 <= b `1 by A6; hence a <= b by A8, A9, Th11; ::_thesis: verum end; hence ex_sup_of [:D1,D2:],[:S1,S2:] by YELLOW_0:15; ::_thesis: verum end; assume ex_sup_of [:D1,D2:],[:S1,S2:] ; ::_thesis: ( ex_sup_of D1,S1 & ex_sup_of D2,S2 ) then consider x being Element of [:S1,S2:] such that A10: [:D1,D2:] is_<=_than x and A11: for b being Element of [:S1,S2:] st [:D1,D2:] is_<=_than b holds x <= b by YELLOW_0:15; the carrier of [:S1,S2:] = [: the carrier of S1, the carrier of S2:] by Def2; then A12: x = [(x `1),(x `2)] by MCART_1:21; then A13: D1 is_<=_than x `1 by A10, Th29; A14: D2 is_<=_than x `2 by A10, A12, Th29; for b being Element of S1 st D1 is_<=_than b holds x `1 <= b proof let b be Element of S1; ::_thesis: ( D1 is_<=_than b implies x `1 <= b ) assume D1 is_<=_than b ; ::_thesis: x `1 <= b then x <= [b,(x `2)] by A11, A14, Th30; hence x `1 <= b by A12, Th11; ::_thesis: verum end; hence ex_sup_of D1,S1 by A13, YELLOW_0:15; ::_thesis: ex_sup_of D2,S2 for b being Element of S2 st D2 is_<=_than b holds x `2 <= b proof let b be Element of S2; ::_thesis: ( D2 is_<=_than b implies x `2 <= b ) assume D2 is_<=_than b ; ::_thesis: x `2 <= b then x <= [(x `1),b] by A11, A13, Th30; hence x `2 <= b by A12, Th11; ::_thesis: verum end; hence ex_sup_of D2,S2 by A14, YELLOW_0:15; ::_thesis: verum end; theorem Th40: :: YELLOW_3:40 for S1, S2 being non empty antisymmetric RelStr for D1 being non empty Subset of S1 for D2 being non empty Subset of S2 holds ( ( ex_inf_of D1,S1 & ex_inf_of D2,S2 ) iff ex_inf_of [:D1,D2:],[:S1,S2:] ) proof let S1, S2 be non empty antisymmetric RelStr ; ::_thesis: for D1 being non empty Subset of S1 for D2 being non empty Subset of S2 holds ( ( ex_inf_of D1,S1 & ex_inf_of D2,S2 ) iff ex_inf_of [:D1,D2:],[:S1,S2:] ) let D1 be non empty Subset of S1; ::_thesis: for D2 being non empty Subset of S2 holds ( ( ex_inf_of D1,S1 & ex_inf_of D2,S2 ) iff ex_inf_of [:D1,D2:],[:S1,S2:] ) let D2 be non empty Subset of S2; ::_thesis: ( ( ex_inf_of D1,S1 & ex_inf_of D2,S2 ) iff ex_inf_of [:D1,D2:],[:S1,S2:] ) hereby ::_thesis: ( ex_inf_of [:D1,D2:],[:S1,S2:] implies ( ex_inf_of D1,S1 & ex_inf_of D2,S2 ) ) assume that A1: ex_inf_of D1,S1 and A2: ex_inf_of D2,S2 ; ::_thesis: ex_inf_of [:D1,D2:],[:S1,S2:] consider a2 being Element of S2 such that A3: D2 is_>=_than a2 and A4: for b being Element of S2 st D2 is_>=_than b holds a2 >= b by A2, YELLOW_0:16; consider a1 being Element of S1 such that A5: D1 is_>=_than a1 and A6: for b being Element of S1 st D1 is_>=_than b holds a1 >= b by A1, YELLOW_0:16; ex a being Element of [:S1,S2:] st ( [:D1,D2:] is_>=_than a & ( for b being Element of [:S1,S2:] st [:D1,D2:] is_>=_than b holds a >= b ) ) proof take a = [a1,a2]; ::_thesis: ( [:D1,D2:] is_>=_than a & ( for b being Element of [:S1,S2:] st [:D1,D2:] is_>=_than b holds a >= b ) ) thus [:D1,D2:] is_>=_than a by A5, A3, Th33; ::_thesis: for b being Element of [:S1,S2:] st [:D1,D2:] is_>=_than b holds a >= b let b be Element of [:S1,S2:]; ::_thesis: ( [:D1,D2:] is_>=_than b implies a >= b ) assume A7: [:D1,D2:] is_>=_than b ; ::_thesis: a >= b the carrier of [:S1,S2:] = [: the carrier of S1, the carrier of S2:] by Def2; then A8: b = [(b `1),(b `2)] by MCART_1:21; then D2 is_>=_than b `2 by A7, Th32; then A9: a2 >= b `2 by A4; D1 is_>=_than b `1 by A7, A8, Th32; then a1 >= b `1 by A6; hence a >= b by A8, A9, Th11; ::_thesis: verum end; hence ex_inf_of [:D1,D2:],[:S1,S2:] by YELLOW_0:16; ::_thesis: verum end; assume ex_inf_of [:D1,D2:],[:S1,S2:] ; ::_thesis: ( ex_inf_of D1,S1 & ex_inf_of D2,S2 ) then consider x being Element of [:S1,S2:] such that A10: [:D1,D2:] is_>=_than x and A11: for b being Element of [:S1,S2:] st [:D1,D2:] is_>=_than b holds x >= b by YELLOW_0:16; the carrier of [:S1,S2:] = [: the carrier of S1, the carrier of S2:] by Def2; then A12: x = [(x `1),(x `2)] by MCART_1:21; then A13: D1 is_>=_than x `1 by A10, Th32; A14: D2 is_>=_than x `2 by A10, A12, Th32; for b being Element of S1 st D1 is_>=_than b holds x `1 >= b proof let b be Element of S1; ::_thesis: ( D1 is_>=_than b implies x `1 >= b ) assume D1 is_>=_than b ; ::_thesis: x `1 >= b then x >= [b,(x `2)] by A11, A14, Th33; hence x `1 >= b by A12, Th11; ::_thesis: verum end; hence ex_inf_of D1,S1 by A13, YELLOW_0:16; ::_thesis: ex_inf_of D2,S2 for b being Element of S2 st D2 is_>=_than b holds x `2 >= b proof let b be Element of S2; ::_thesis: ( D2 is_>=_than b implies x `2 >= b ) assume D2 is_>=_than b ; ::_thesis: x `2 >= b then x >= [(x `1),b] by A11, A13, Th33; hence x `2 >= b by A12, Th11; ::_thesis: verum end; hence ex_inf_of D2,S2 by A14, YELLOW_0:16; ::_thesis: verum end; theorem Th41: :: YELLOW_3:41 for S1, S2 being non empty antisymmetric RelStr for D being Subset of [:S1,S2:] holds ( ( ex_sup_of proj1 D,S1 & ex_sup_of proj2 D,S2 ) iff ex_sup_of D,[:S1,S2:] ) proof let S1, S2 be non empty antisymmetric RelStr ; ::_thesis: for D being Subset of [:S1,S2:] holds ( ( ex_sup_of proj1 D,S1 & ex_sup_of proj2 D,S2 ) iff ex_sup_of D,[:S1,S2:] ) let D be Subset of [:S1,S2:]; ::_thesis: ( ( ex_sup_of proj1 D,S1 & ex_sup_of proj2 D,S2 ) iff ex_sup_of D,[:S1,S2:] ) A1: the carrier of [:S1,S2:] = [: the carrier of S1, the carrier of S2:] by Def2; then A2: D c= [:(proj1 D),(proj2 D):] by Th1; hereby ::_thesis: ( ex_sup_of D,[:S1,S2:] implies ( ex_sup_of proj1 D,S1 & ex_sup_of proj2 D,S2 ) ) assume that A3: ex_sup_of proj1 D,S1 and A4: ex_sup_of proj2 D,S2 ; ::_thesis: ex_sup_of D,[:S1,S2:] ex a being Element of [:S1,S2:] st ( D is_<=_than a & ( for b being Element of [:S1,S2:] st D is_<=_than b holds a <= b ) ) proof consider x2 being Element of S2 such that A5: proj2 D is_<=_than x2 and A6: for b being Element of S2 st proj2 D is_<=_than b holds x2 <= b by A4, YELLOW_0:15; consider x1 being Element of S1 such that A7: proj1 D is_<=_than x1 and A8: for b being Element of S1 st proj1 D is_<=_than b holds x1 <= b by A3, YELLOW_0:15; take a = [x1,x2]; ::_thesis: ( D is_<=_than a & ( for b being Element of [:S1,S2:] st D is_<=_than b holds a <= b ) ) thus D is_<=_than a ::_thesis: for b being Element of [:S1,S2:] st D is_<=_than b holds a <= b proof let q be Element of [:S1,S2:]; :: according to LATTICE3:def_9 ::_thesis: ( not q in D or q <= a ) assume q in D ; ::_thesis: q <= a then consider q1, q2 being set such that A9: q1 in proj1 D and A10: q2 in proj2 D and A11: q = [q1,q2] by A2, ZFMISC_1:def_2; reconsider q2 = q2 as Element of S2 by A10; reconsider q1 = q1 as Element of S1 by A9; ( q1 <= x1 & q2 <= x2 ) by A7, A5, A9, A10, LATTICE3:def_9; hence q <= a by A11, Th11; ::_thesis: verum end; let b be Element of [:S1,S2:]; ::_thesis: ( D is_<=_than b implies a <= b ) assume A12: D is_<=_than b ; ::_thesis: a <= b A13: b = [(b `1),(b `2)] by A1, MCART_1:21; then proj2 D is_<=_than b `2 by A12, Th31; then A14: x2 <= b `2 by A6; proj1 D is_<=_than b `1 by A12, A13, Th31; then x1 <= b `1 by A8; hence a <= b by A13, A14, Th11; ::_thesis: verum end; hence ex_sup_of D,[:S1,S2:] by YELLOW_0:15; ::_thesis: verum end; assume ex_sup_of D,[:S1,S2:] ; ::_thesis: ( ex_sup_of proj1 D,S1 & ex_sup_of proj2 D,S2 ) then consider x being Element of [:S1,S2:] such that A15: D is_<=_than x and A16: for b being Element of [:S1,S2:] st D is_<=_than b holds x <= b by YELLOW_0:15; A17: x = [(x `1),(x `2)] by A1, MCART_1:21; then A18: proj1 D is_<=_than x `1 by A15, Th31; A19: proj2 D is_<=_than x `2 by A15, A17, Th31; for b being Element of S1 st proj1 D is_<=_than b holds x `1 <= b proof let b be Element of S1; ::_thesis: ( proj1 D is_<=_than b implies x `1 <= b ) assume proj1 D is_<=_than b ; ::_thesis: x `1 <= b then D is_<=_than [b,(x `2)] by A19, Th31; then x <= [b,(x `2)] by A16; hence x `1 <= b by A17, Th11; ::_thesis: verum end; hence ex_sup_of proj1 D,S1 by A18, YELLOW_0:15; ::_thesis: ex_sup_of proj2 D,S2 for b being Element of S2 st proj2 D is_<=_than b holds x `2 <= b proof let b be Element of S2; ::_thesis: ( proj2 D is_<=_than b implies x `2 <= b ) assume proj2 D is_<=_than b ; ::_thesis: x `2 <= b then D is_<=_than [(x `1),b] by A18, Th31; then x <= [(x `1),b] by A16; hence x `2 <= b by A17, Th11; ::_thesis: verum end; hence ex_sup_of proj2 D,S2 by A19, YELLOW_0:15; ::_thesis: verum end; theorem Th42: :: YELLOW_3:42 for S1, S2 being non empty antisymmetric RelStr for D being Subset of [:S1,S2:] holds ( ( ex_inf_of proj1 D,S1 & ex_inf_of proj2 D,S2 ) iff ex_inf_of D,[:S1,S2:] ) proof let S1, S2 be non empty antisymmetric RelStr ; ::_thesis: for D being Subset of [:S1,S2:] holds ( ( ex_inf_of proj1 D,S1 & ex_inf_of proj2 D,S2 ) iff ex_inf_of D,[:S1,S2:] ) let D be Subset of [:S1,S2:]; ::_thesis: ( ( ex_inf_of proj1 D,S1 & ex_inf_of proj2 D,S2 ) iff ex_inf_of D,[:S1,S2:] ) A1: the carrier of [:S1,S2:] = [: the carrier of S1, the carrier of S2:] by Def2; then A2: D c= [:(proj1 D),(proj2 D):] by Th1; hereby ::_thesis: ( ex_inf_of D,[:S1,S2:] implies ( ex_inf_of proj1 D,S1 & ex_inf_of proj2 D,S2 ) ) assume that A3: ex_inf_of proj1 D,S1 and A4: ex_inf_of proj2 D,S2 ; ::_thesis: ex_inf_of D,[:S1,S2:] ex a being Element of [:S1,S2:] st ( D is_>=_than a & ( for b being Element of [:S1,S2:] st D is_>=_than b holds a >= b ) ) proof consider x2 being Element of S2 such that A5: proj2 D is_>=_than x2 and A6: for b being Element of S2 st proj2 D is_>=_than b holds x2 >= b by A4, YELLOW_0:16; consider x1 being Element of S1 such that A7: proj1 D is_>=_than x1 and A8: for b being Element of S1 st proj1 D is_>=_than b holds x1 >= b by A3, YELLOW_0:16; take a = [x1,x2]; ::_thesis: ( D is_>=_than a & ( for b being Element of [:S1,S2:] st D is_>=_than b holds a >= b ) ) thus D is_>=_than a ::_thesis: for b being Element of [:S1,S2:] st D is_>=_than b holds a >= b proof let q be Element of [:S1,S2:]; :: according to LATTICE3:def_8 ::_thesis: ( not q in D or a <= q ) assume q in D ; ::_thesis: a <= q then consider q1, q2 being set such that A9: q1 in proj1 D and A10: q2 in proj2 D and A11: q = [q1,q2] by A2, ZFMISC_1:def_2; reconsider q2 = q2 as Element of S2 by A10; reconsider q1 = q1 as Element of S1 by A9; ( q1 >= x1 & q2 >= x2 ) by A7, A5, A9, A10, LATTICE3:def_8; hence a <= q by A11, Th11; ::_thesis: verum end; let b be Element of [:S1,S2:]; ::_thesis: ( D is_>=_than b implies a >= b ) assume A12: D is_>=_than b ; ::_thesis: a >= b A13: b = [(b `1),(b `2)] by A1, MCART_1:21; then proj2 D is_>=_than b `2 by A12, Th34; then A14: x2 >= b `2 by A6; proj1 D is_>=_than b `1 by A12, A13, Th34; then x1 >= b `1 by A8; hence a >= b by A13, A14, Th11; ::_thesis: verum end; hence ex_inf_of D,[:S1,S2:] by YELLOW_0:16; ::_thesis: verum end; assume ex_inf_of D,[:S1,S2:] ; ::_thesis: ( ex_inf_of proj1 D,S1 & ex_inf_of proj2 D,S2 ) then consider x being Element of [:S1,S2:] such that A15: D is_>=_than x and A16: for b being Element of [:S1,S2:] st D is_>=_than b holds x >= b by YELLOW_0:16; A17: x = [(x `1),(x `2)] by A1, MCART_1:21; then A18: proj1 D is_>=_than x `1 by A15, Th34; A19: proj2 D is_>=_than x `2 by A15, A17, Th34; for b being Element of S1 st proj1 D is_>=_than b holds x `1 >= b proof let b be Element of S1; ::_thesis: ( proj1 D is_>=_than b implies x `1 >= b ) assume proj1 D is_>=_than b ; ::_thesis: x `1 >= b then D is_>=_than [b,(x `2)] by A19, Th34; then x >= [b,(x `2)] by A16; hence x `1 >= b by A17, Th11; ::_thesis: verum end; hence ex_inf_of proj1 D,S1 by A18, YELLOW_0:16; ::_thesis: ex_inf_of proj2 D,S2 for b being Element of S2 st proj2 D is_>=_than b holds x `2 >= b proof let b be Element of S2; ::_thesis: ( proj2 D is_>=_than b implies x `2 >= b ) assume proj2 D is_>=_than b ; ::_thesis: x `2 >= b then D is_>=_than [(x `1),b] by A18, Th34; then x >= [(x `1),b] by A16; hence x `2 >= b by A17, Th11; ::_thesis: verum end; hence ex_inf_of proj2 D,S2 by A19, YELLOW_0:16; ::_thesis: verum end; theorem Th43: :: YELLOW_3:43 for S1, S2 being non empty antisymmetric RelStr for D1 being non empty Subset of S1 for D2 being non empty Subset of S2 st ex_sup_of D1,S1 & ex_sup_of D2,S2 holds sup [:D1,D2:] = [(sup D1),(sup D2)] proof let S1, S2 be non empty antisymmetric RelStr ; ::_thesis: for D1 being non empty Subset of S1 for D2 being non empty Subset of S2 st ex_sup_of D1,S1 & ex_sup_of D2,S2 holds sup [:D1,D2:] = [(sup D1),(sup D2)] let D1 be non empty Subset of S1; ::_thesis: for D2 being non empty Subset of S2 st ex_sup_of D1,S1 & ex_sup_of D2,S2 holds sup [:D1,D2:] = [(sup D1),(sup D2)] let D2 be non empty Subset of S2; ::_thesis: ( ex_sup_of D1,S1 & ex_sup_of D2,S2 implies sup [:D1,D2:] = [(sup D1),(sup D2)] ) assume A1: ( ex_sup_of D1,S1 & ex_sup_of D2,S2 ) ; ::_thesis: sup [:D1,D2:] = [(sup D1),(sup D2)] set s = sup [:D1,D2:]; sup [:D1,D2:] is Element of [: the carrier of S1, the carrier of S2:] by Def2; then consider s1, s2 being set such that A2: s1 in the carrier of S1 and A3: s2 in the carrier of S2 and A4: sup [:D1,D2:] = [s1,s2] by ZFMISC_1:def_2; reconsider s2 = s2 as Element of S2 by A3; reconsider s1 = s1 as Element of S1 by A2; A5: ex_sup_of [:D1,D2:],[:S1,S2:] by A1, Th39; then A6: [s1,s2] is_>=_than [:D1,D2:] by A4, YELLOW_0:30; then A7: s1 is_>=_than D1 by Th29; A8: for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds [s1,s2] <= b by A4, A5, YELLOW_0:30; then for b being Element of S1 st b is_>=_than D1 holds s1 <= b by A1, Th35; then A9: s1 = sup D1 by A7, YELLOW_0:30; A10: s2 is_>=_than D2 by A6, Th29; for b being Element of S2 st b is_>=_than D2 holds s2 <= b by A1, A8, Th35; hence sup [:D1,D2:] = [(sup D1),(sup D2)] by A4, A9, A10, YELLOW_0:30; ::_thesis: verum end; theorem Th44: :: YELLOW_3:44 for S1, S2 being non empty antisymmetric RelStr for D1 being non empty Subset of S1 for D2 being non empty Subset of S2 st ex_inf_of D1,S1 & ex_inf_of D2,S2 holds inf [:D1,D2:] = [(inf D1),(inf D2)] proof let S1, S2 be non empty antisymmetric RelStr ; ::_thesis: for D1 being non empty Subset of S1 for D2 being non empty Subset of S2 st ex_inf_of D1,S1 & ex_inf_of D2,S2 holds inf [:D1,D2:] = [(inf D1),(inf D2)] let D1 be non empty Subset of S1; ::_thesis: for D2 being non empty Subset of S2 st ex_inf_of D1,S1 & ex_inf_of D2,S2 holds inf [:D1,D2:] = [(inf D1),(inf D2)] let D2 be non empty Subset of S2; ::_thesis: ( ex_inf_of D1,S1 & ex_inf_of D2,S2 implies inf [:D1,D2:] = [(inf D1),(inf D2)] ) assume A1: ( ex_inf_of D1,S1 & ex_inf_of D2,S2 ) ; ::_thesis: inf [:D1,D2:] = [(inf D1),(inf D2)] set s = inf [:D1,D2:]; inf [:D1,D2:] is Element of [: the carrier of S1, the carrier of S2:] by Def2; then consider s1, s2 being set such that A2: s1 in the carrier of S1 and A3: s2 in the carrier of S2 and A4: inf [:D1,D2:] = [s1,s2] by ZFMISC_1:def_2; reconsider s2 = s2 as Element of S2 by A3; reconsider s1 = s1 as Element of S1 by A2; A5: ex_inf_of [:D1,D2:],[:S1,S2:] by A1, Th40; then A6: [s1,s2] is_<=_than [:D1,D2:] by A4, YELLOW_0:31; then A7: s1 is_<=_than D1 by Th32; A8: for b being Element of [:S1,S2:] st b is_<=_than [:D1,D2:] holds [s1,s2] >= b by A4, A5, YELLOW_0:31; then for b being Element of S1 st b is_<=_than D1 holds s1 >= b by A1, Th36; then A9: s1 = inf D1 by A7, YELLOW_0:31; A10: s2 is_<=_than D2 by A6, Th32; for b being Element of S2 st b is_<=_than D2 holds s2 >= b by A1, A8, Th36; hence inf [:D1,D2:] = [(inf D1),(inf D2)] by A4, A9, A10, YELLOW_0:31; ::_thesis: verum end; registration let X, Y be non empty antisymmetric complete RelStr ; cluster[:X,Y:] -> strict complete ; coherence [:X,Y:] is complete proof set IT = [:X,Y:]; for D being Subset of [:X,Y:] holds ex_sup_of D,[:X,Y:] proof let D be Subset of [:X,Y:]; ::_thesis: ex_sup_of D,[:X,Y:] ( ex_sup_of proj1 D,X & ex_sup_of proj2 D,Y ) by YELLOW_0:17; hence ex_sup_of D,[:X,Y:] by Th41; ::_thesis: verum end; hence [:X,Y:] is complete by YELLOW_0:53; ::_thesis: verum end; end; theorem :: YELLOW_3:45 for X, Y being non empty antisymmetric lower-bounded RelStr st [:X,Y:] is complete holds ( X is complete & Y is complete ) proof let X, Y be non empty antisymmetric lower-bounded RelStr ; ::_thesis: ( [:X,Y:] is complete implies ( X is complete & Y is complete ) ) assume A1: [:X,Y:] is complete ; ::_thesis: ( X is complete & Y is complete ) for A being Subset of X holds ex_sup_of A,X proof let A be Subset of X; ::_thesis: ex_sup_of A,X percases ( not A is empty or A is empty ) ; supposeA2: not A is empty ; ::_thesis: ex_sup_of A,X set B = the non empty Subset of Y; ex_sup_of [:A, the non empty Subset of Y:],[:X,Y:] by A1, YELLOW_0:17; hence ex_sup_of A,X by A2, Th39; ::_thesis: verum end; suppose A is empty ; ::_thesis: ex_sup_of A,X hence ex_sup_of A,X by YELLOW_0:42; ::_thesis: verum end; end; end; hence X is complete by YELLOW_0:53; ::_thesis: Y is complete for B being Subset of Y holds ex_sup_of B,Y proof let B be Subset of Y; ::_thesis: ex_sup_of B,Y percases ( not B is empty or B is empty ) ; supposeA3: not B is empty ; ::_thesis: ex_sup_of B,Y set A = the non empty Subset of X; ex_sup_of [: the non empty Subset of X,B:],[:X,Y:] by A1, YELLOW_0:17; hence ex_sup_of B,Y by A3, Th39; ::_thesis: verum end; suppose B is empty ; ::_thesis: ex_sup_of B,Y hence ex_sup_of B,Y by YELLOW_0:42; ::_thesis: verum end; end; end; hence Y is complete by YELLOW_0:53; ::_thesis: verum end; theorem :: YELLOW_3:46 for L1, L2 being non empty antisymmetric RelStr for D being non empty Subset of [:L1,L2:] st ( [:L1,L2:] is complete or ex_sup_of D,[:L1,L2:] ) holds sup D = [(sup (proj1 D)),(sup (proj2 D))] proof let L1, L2 be non empty antisymmetric RelStr ; ::_thesis: for D being non empty Subset of [:L1,L2:] st ( [:L1,L2:] is complete or ex_sup_of D,[:L1,L2:] ) holds sup D = [(sup (proj1 D)),(sup (proj2 D))] let D be non empty Subset of [:L1,L2:]; ::_thesis: ( ( [:L1,L2:] is complete or ex_sup_of D,[:L1,L2:] ) implies sup D = [(sup (proj1 D)),(sup (proj2 D))] ) reconsider C1 = the carrier of L1, C2 = the carrier of L2 as non empty set ; the carrier of [:L1,L2:] = [:C1,C2:] by Def2; then consider d1, d2 being set such that A1: d1 in C1 and A2: d2 in C2 and A3: sup D = [d1,d2] by ZFMISC_1:def_2; reconsider d1 = d1 as Element of L1 by A1; reconsider D9 = D as non empty Subset of [:C1,C2:] by Def2; not proj1 D9 is empty ; then reconsider D1 = proj1 D as non empty Subset of L1 ; not proj2 D9 is empty ; then reconsider D2 = proj2 D as non empty Subset of L2 ; A4: D9 c= [:D1,D2:] by Th1; reconsider d2 = d2 as Element of L2 by A2; assume ( [:L1,L2:] is complete or ex_sup_of D,[:L1,L2:] ) ; ::_thesis: sup D = [(sup (proj1 D)),(sup (proj2 D))] then A5: ex_sup_of D,[:L1,L2:] by YELLOW_0:17; then A6: ex_sup_of D2,L2 by Th41; A7: ex_sup_of D1,L1 by A5, Th41; then ex_sup_of [:D1,D2:],[:L1,L2:] by A6, Th39; then sup D <= sup [:D1,D2:] by A5, A4, YELLOW_0:34; then A8: sup D <= [(sup (proj1 D)),(sup (proj2 D))] by A7, A6, Th43; D2 is_<=_than d2 proof let b be Element of L2; :: according to LATTICE3:def_9 ::_thesis: ( not b in D2 or b <= d2 ) assume b in D2 ; ::_thesis: b <= d2 then consider x being set such that A9: [x,b] in D by XTUPLE_0:def_13; reconsider x = x as Element of D1 by A9, XTUPLE_0:def_12; reconsider x = x as Element of L1 ; D is_<=_than [d1,d2] by A5, A3, YELLOW_0:def_9; then [x,b] <= [d1,d2] by A9, LATTICE3:def_9; hence b <= d2 by Th11; ::_thesis: verum end; then A10: sup D2 <= d2 by A6, YELLOW_0:def_9; D1 is_<=_than d1 proof let b be Element of L1; :: according to LATTICE3:def_9 ::_thesis: ( not b in D1 or b <= d1 ) assume b in D1 ; ::_thesis: b <= d1 then consider x being set such that A11: [b,x] in D by XTUPLE_0:def_12; reconsider x = x as Element of D2 by A11, XTUPLE_0:def_13; reconsider x = x as Element of L2 ; D is_<=_than [d1,d2] by A5, A3, YELLOW_0:def_9; then [b,x] <= [d1,d2] by A11, LATTICE3:def_9; hence b <= d1 by Th11; ::_thesis: verum end; then sup D1 <= d1 by A7, YELLOW_0:def_9; then [(sup D1),(sup D2)] <= sup D by A3, A10, Th11; hence sup D = [(sup (proj1 D)),(sup (proj2 D))] by A8, ORDERS_2:2; ::_thesis: verum end; theorem :: YELLOW_3:47 for L1, L2 being non empty antisymmetric RelStr for D being non empty Subset of [:L1,L2:] st ( [:L1,L2:] is complete or ex_inf_of D,[:L1,L2:] ) holds inf D = [(inf (proj1 D)),(inf (proj2 D))] proof let L1, L2 be non empty antisymmetric RelStr ; ::_thesis: for D being non empty Subset of [:L1,L2:] st ( [:L1,L2:] is complete or ex_inf_of D,[:L1,L2:] ) holds inf D = [(inf (proj1 D)),(inf (proj2 D))] let D be non empty Subset of [:L1,L2:]; ::_thesis: ( ( [:L1,L2:] is complete or ex_inf_of D,[:L1,L2:] ) implies inf D = [(inf (proj1 D)),(inf (proj2 D))] ) reconsider C1 = the carrier of L1, C2 = the carrier of L2 as non empty set ; the carrier of [:L1,L2:] = [:C1,C2:] by Def2; then consider d1, d2 being set such that A1: d1 in C1 and A2: d2 in C2 and A3: inf D = [d1,d2] by ZFMISC_1:def_2; reconsider d1 = d1 as Element of L1 by A1; reconsider D9 = D as non empty Subset of [:C1,C2:] by Def2; not proj1 D9 is empty ; then reconsider D1 = proj1 D as non empty Subset of L1 ; not proj2 D9 is empty ; then reconsider D2 = proj2 D as non empty Subset of L2 ; A4: D9 c= [:D1,D2:] by Th1; reconsider d2 = d2 as Element of L2 by A2; assume ( [:L1,L2:] is complete or ex_inf_of D,[:L1,L2:] ) ; ::_thesis: inf D = [(inf (proj1 D)),(inf (proj2 D))] then A5: ex_inf_of D,[:L1,L2:] by YELLOW_0:17; then A6: ex_inf_of D2,L2 by Th42; A7: ex_inf_of D1,L1 by A5, Th42; then ex_inf_of [:D1,D2:],[:L1,L2:] by A6, Th40; then inf D >= inf [:D1,D2:] by A5, A4, YELLOW_0:35; then A8: inf D >= [(inf (proj1 D)),(inf (proj2 D))] by A7, A6, Th44; D2 is_>=_than d2 proof let b be Element of L2; :: according to LATTICE3:def_8 ::_thesis: ( not b in D2 or d2 <= b ) assume b in D2 ; ::_thesis: d2 <= b then consider x being set such that A9: [x,b] in D by XTUPLE_0:def_13; reconsider x = x as Element of D1 by A9, XTUPLE_0:def_12; reconsider x = x as Element of L1 ; D is_>=_than [d1,d2] by A5, A3, YELLOW_0:def_10; then [x,b] >= [d1,d2] by A9, LATTICE3:def_8; hence d2 <= b by Th11; ::_thesis: verum end; then A10: inf D2 >= d2 by A6, YELLOW_0:def_10; D1 is_>=_than d1 proof let b be Element of L1; :: according to LATTICE3:def_8 ::_thesis: ( not b in D1 or d1 <= b ) assume b in D1 ; ::_thesis: d1 <= b then consider x being set such that A11: [b,x] in D by XTUPLE_0:def_12; reconsider x = x as Element of D2 by A11, XTUPLE_0:def_13; reconsider x = x as Element of L2 ; D is_>=_than [d1,d2] by A5, A3, YELLOW_0:def_10; then [b,x] >= [d1,d2] by A11, LATTICE3:def_8; hence d1 <= b by Th11; ::_thesis: verum end; then inf D1 >= d1 by A7, YELLOW_0:def_10; then [(inf D1),(inf D2)] >= inf D by A3, A10, Th11; hence inf D = [(inf (proj1 D)),(inf (proj2 D))] by A8, ORDERS_2:2; ::_thesis: verum end; theorem :: YELLOW_3:48 for S1, S2 being non empty reflexive RelStr for D being non empty directed Subset of [:S1,S2:] holds [:(proj1 D),(proj2 D):] c= downarrow D proof let S1, S2 be non empty reflexive RelStr ; ::_thesis: for D being non empty directed Subset of [:S1,S2:] holds [:(proj1 D),(proj2 D):] c= downarrow D let D be non empty directed Subset of [:S1,S2:]; ::_thesis: [:(proj1 D),(proj2 D):] c= downarrow D reconsider C1 = the carrier of S1, C2 = the carrier of S2 as non empty set ; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in [:(proj1 D),(proj2 D):] or q in downarrow D ) reconsider D9 = D as non empty Subset of [:C1,C2:] by Def2; set D1 = proj1 D; set D2 = proj2 D; A1: downarrow D = { x where x is Element of [:S1,S2:] : ex y being Element of [:S1,S2:] st ( x <= y & y in D ) } by WAYBEL_0:14; A2: D9 c= [:(proj1 D),(proj2 D):] by Th1; not proj2 D9 is empty ; then reconsider D2 = proj2 D as non empty Subset of S2 ; not proj1 D9 is empty ; then reconsider D1 = proj1 D as non empty Subset of S1 ; assume q in [:(proj1 D),(proj2 D):] ; ::_thesis: q in downarrow D then consider d, e being set such that A3: d in D1 and A4: e in D2 and A5: q = [d,e] by ZFMISC_1:def_2; consider y being set such that A6: [d,y] in D by A3, XTUPLE_0:def_12; consider x being set such that A7: [x,e] in D by A4, XTUPLE_0:def_13; reconsider y = y, e = e as Element of D2 by A6, A7, XTUPLE_0:def_13; reconsider x = x, d = d as Element of D1 by A6, A7, XTUPLE_0:def_12; consider z being Element of [:S1,S2:] such that A8: z in D and A9: ( [d,y] <= z & [x,e] <= z ) by A6, A7, WAYBEL_0:def_1; consider z1, z2 being set such that A10: z1 in D1 and A11: z2 in D2 and A12: z = [z1,z2] by A2, A8, ZFMISC_1:def_2; reconsider z2 = z2 as Element of D2 by A11; reconsider z1 = z1 as Element of D1 by A10; ( d <= z1 & e <= z2 ) by A9, A10, A11, A12, Th11; then [d,e] <= [z1,z2] by Th11; hence q in downarrow D by A5, A1, A8, A12; ::_thesis: verum end; theorem :: YELLOW_3:49 for S1, S2 being non empty reflexive RelStr for D being non empty filtered Subset of [:S1,S2:] holds [:(proj1 D),(proj2 D):] c= uparrow D proof let S1, S2 be non empty reflexive RelStr ; ::_thesis: for D being non empty filtered Subset of [:S1,S2:] holds [:(proj1 D),(proj2 D):] c= uparrow D let D be non empty filtered Subset of [:S1,S2:]; ::_thesis: [:(proj1 D),(proj2 D):] c= uparrow D reconsider C1 = the carrier of S1, C2 = the carrier of S2 as non empty set ; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in [:(proj1 D),(proj2 D):] or q in uparrow D ) reconsider D9 = D as non empty Subset of [:C1,C2:] by Def2; set D1 = proj1 D; set D2 = proj2 D; A1: uparrow D = { x where x is Element of [:S1,S2:] : ex y being Element of [:S1,S2:] st ( x >= y & y in D ) } by WAYBEL_0:15; A2: D9 c= [:(proj1 D),(proj2 D):] by Th1; not proj2 D9 is empty ; then reconsider D2 = proj2 D as non empty Subset of S2 ; not proj1 D9 is empty ; then reconsider D1 = proj1 D as non empty Subset of S1 ; assume q in [:(proj1 D),(proj2 D):] ; ::_thesis: q in uparrow D then consider d, e being set such that A3: d in D1 and A4: e in D2 and A5: q = [d,e] by ZFMISC_1:def_2; consider y being set such that A6: [d,y] in D by A3, XTUPLE_0:def_12; consider x being set such that A7: [x,e] in D by A4, XTUPLE_0:def_13; reconsider y = y, e = e as Element of D2 by A6, A7, XTUPLE_0:def_13; reconsider x = x, d = d as Element of D1 by A6, A7, XTUPLE_0:def_12; consider z being Element of [:S1,S2:] such that A8: z in D and A9: ( [d,y] >= z & [x,e] >= z ) by A6, A7, WAYBEL_0:def_2; consider z1, z2 being set such that A10: z1 in D1 and A11: z2 in D2 and A12: z = [z1,z2] by A2, A8, ZFMISC_1:def_2; reconsider z2 = z2 as Element of D2 by A11; reconsider z1 = z1 as Element of D1 by A10; ( d >= z1 & e >= z2 ) by A9, A10, A11, A12, Th11; then [d,e] >= [z1,z2] by Th11; hence q in uparrow D by A5, A1, A8, A12; ::_thesis: verum end; scheme :: YELLOW_3:sch 6 Kappa2DS{ F1() -> non empty RelStr , F2() -> non empty RelStr , F3() -> non empty RelStr , F4( set , set ) -> set } : ex f being Function of [:F1(),F2():],F3() st for x being Element of F1() for y being Element of F2() holds f . (x,y) = F4(x,y) provided A1: for x being Element of F1() for y being Element of F2() holds F4(x,y) is Element of F3() proof A2: for x being Element of F1() for y being Element of F2() holds F4(x,y) in the carrier of F3() proof let x be Element of F1(); ::_thesis: for y being Element of F2() holds F4(x,y) in the carrier of F3() let y be Element of F2(); ::_thesis: F4(x,y) in the carrier of F3() reconsider x1 = x as Element of F1() ; reconsider y1 = y as Element of F2() ; F4(x1,y1) is Element of F3() by A1; hence F4(x,y) in the carrier of F3() ; ::_thesis: verum end; consider f being Function of [: the carrier of F1(), the carrier of F2():], the carrier of F3() such that A3: for x being Element of F1() for y being Element of F2() holds f . (x,y) = F4(x,y) from FUNCT_7:sch_1(A2); the carrier of [:F1(),F2():] = [: the carrier of F1(), the carrier of F2():] by Def2; then reconsider f = f as Function of [:F1(),F2():],F3() ; take f ; ::_thesis: for x being Element of F1() for y being Element of F2() holds f . (x,y) = F4(x,y) thus for x being Element of F1() for y being Element of F2() holds f . (x,y) = F4(x,y) by A3; ::_thesis: verum end;