Copyright (c) 1998 Association of Mizar Users
environ vocabulary LATTICES, ORDERS_1, LATTICE3, RELAT_2, YELLOW_0, BOOLE, BHSP_3, ORDINAL2, FUNCT_5, MCART_1, WAYBEL_0, WAYBEL_3, QUANTAL1, COMPTS_1, WAYBEL_8, WAYBEL_6, WAYBEL11, WAYBEL_2; notation TARSKI, XBOOLE_0, ZFMISC_1, STRUCT_0, MCART_1, ORDERS_1, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_1, YELLOW_3, YELLOW_4, WAYBEL_2, WAYBEL_3, WAYBEL_6, WAYBEL_8, WAYBEL11; constructors YELLOW_4, WAYBEL_1, WAYBEL_3, WAYBEL_6, WAYBEL_8, ORDERS_3, WAYBEL11; clusters STRUCT_0, LATTICE3, YELLOW_0, YELLOW_3, YELLOW_4, WAYBEL_0, WAYBEL_2, WAYBEL_3, WAYBEL_8, WAYBEL14, SUBSET_1, XBOOLE_0; requirements SUBSET, BOOLE; definitions TARSKI, YELLOW_0, LATTICE3, WAYBEL_0, WAYBEL_1, WAYBEL_2, WAYBEL_3, WAYBEL_6, WAYBEL_8, WAYBEL11, XBOOLE_0; theorems STRUCT_0, ZFMISC_1, TARSKI, ORDERS_1, YELLOW_0, YELLOW_3, YELLOW_4, WAYBEL_0, WAYBEL_1, WAYBEL_2, WAYBEL_3, WAYBEL_8, MCART_1, FUNCT_5, DOMAIN_1, XBOOLE_0; begin :: On the elements of product of relational structures definition let S, T be non empty upper-bounded RelStr; cluster [:S,T:] -> upper-bounded; coherence proof consider s being Element of S such that A1: s is_>=_than the carrier of S by YELLOW_0:def 5; consider t being Element of T such that A2: t is_>=_than the carrier of T by YELLOW_0:def 5; take [s,t]; A3: the carrier of [:S,T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2; the carrier of S c= the carrier of S & the carrier of T c= the carrier of T; then the carrier of S is Subset of S & the carrier of T is Subset of T ; hence thesis by A1,A2,A3,YELLOW_3:30; end; end; definition let S, T be non empty lower-bounded RelStr; cluster [:S,T:] -> lower-bounded; coherence proof consider s being Element of S such that A1: s is_<=_than the carrier of S by YELLOW_0:def 4; consider t being Element of T such that A2: t is_<=_than the carrier of T by YELLOW_0:def 4; take [s,t]; A3: the carrier of [:S,T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2; the carrier of S c= the carrier of S & the carrier of T c= the carrier of T; then the carrier of S is Subset of S & the carrier of T is Subset of T ; hence thesis by A1,A2,A3,YELLOW_3:33; end; end; theorem for S, T being non empty RelStr st [:S,T:] is upper-bounded holds S is upper-bounded & T is upper-bounded proof let S, T be non empty RelStr; given x being Element of [:S,T:] such that A1: x is_>=_than the carrier of [:S,T:]; the carrier of [:S,T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2; then consider s, t being set such that A2: s in the carrier of S & t in the carrier of T & x = [s,t] by ZFMISC_1:def 2; reconsider s as Element of S by A2; reconsider t as Element of T by A2; the carrier of S c= the carrier of S & the carrier of T c= the carrier of T; then A3: the carrier of S is non empty Subset of S & the carrier of T is non empty Subset of T; A4: [s,t] is_>=_than [:the carrier of S,the carrier of T:] by A1,A2,YELLOW_3:def 2; thus S is upper-bounded proof take s; thus thesis by A3,A4,YELLOW_3:29; end; take t; thus thesis by A3,A4,YELLOW_3:29; end; theorem for S, T being non empty RelStr st [:S,T:] is lower-bounded holds S is lower-bounded & T is lower-bounded proof let S, T be non empty RelStr; given x being Element of [:S,T:] such that A1: x is_<=_than the carrier of [:S,T:]; the carrier of [:S,T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2; then consider s, t being set such that A2: s in the carrier of S & t in the carrier of T & x = [s,t] by ZFMISC_1:def 2; reconsider s as Element of S by A2; reconsider t as Element of T by A2; the carrier of S c= the carrier of S & the carrier of T c= the carrier of T; then A3: the carrier of S is non empty Subset of S & the carrier of T is non empty Subset of T; A4: [s,t] is_<=_than [:the carrier of S,the carrier of T:] by A1,A2,YELLOW_3:def 2; thus S is lower-bounded proof take s; thus thesis by A3,A4,YELLOW_3:32; end; take t; thus thesis by A3,A4,YELLOW_3:32; end; theorem Th3: for S, T being upper-bounded antisymmetric non empty RelStr holds Top [:S,T:] = [Top S,Top T] proof let S, T be upper-bounded antisymmetric non empty RelStr; A1: ex_inf_of {},[:S,T:] by YELLOW_0:43; A2: {} is_>=_than [Top S,Top T] by YELLOW_0:6; for a being Element of [:S,T:] st {} is_>=_than a holds a <= [Top S,Top T ] proof let a be Element of [:S,T:]; assume {} is_>=_than a; the carrier of [:S,T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2; then consider s, t being set such that A3: s in the carrier of S & t in the carrier of T & a = [s,t] by ZFMISC_1:def 2; reconsider s as Element of S by A3; reconsider t as Element of T by A3; s <= Top S & t <= Top T by YELLOW_0:45; hence a <= [Top S,Top T] by A3,YELLOW_3:11; end; then [Top S,Top T] = "/\"({},[:S,T:]) by A1,A2,YELLOW_0:def 10; hence Top [:S,T:] = [Top S,Top T] by YELLOW_0:def 12; end; theorem Th4: for S, T being lower-bounded antisymmetric non empty RelStr holds Bottom [:S,T:] = [Bottom S,Bottom T] proof let S, T be lower-bounded antisymmetric non empty RelStr; A1: ex_sup_of {},[:S,T:] by YELLOW_0:42; A2: {} is_<=_than [Bottom S,Bottom T] by YELLOW_0:6; for a being Element of [:S,T:] st {} is_<=_than a holds [Bottom S,Bottom T] <= a proof let a be Element of [:S,T:]; assume {} is_<=_than a; the carrier of [:S,T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2; then consider s, t being set such that A3: s in the carrier of S & t in the carrier of T & a = [s,t] by ZFMISC_1:def 2; reconsider s as Element of S by A3; reconsider t as Element of T by A3; Bottom S <= s & Bottom T <= t by YELLOW_0:44; hence [Bottom S,Bottom T] <= a by A3,YELLOW_3:11; end; then [Bottom S,Bottom T] = "\/"({},[:S,T:]) by A1,A2,YELLOW_0:def 9; hence Bottom [:S,T:] = [Bottom S,Bottom T] by YELLOW_0:def 11; end; theorem Th5: for S, T being lower-bounded antisymmetric non empty RelStr, D being Subset of [:S,T:] st [:S,T:] is complete or ex_sup_of D,[:S,T:] holds sup D = [sup proj1 D,sup proj2 D] proof let S, T be lower-bounded antisymmetric non empty RelStr, D be Subset of [:S,T:] such that A1: [:S,T:] is complete or ex_sup_of D,[:S,T:]; per cases; suppose D <> {}; hence thesis by A1,YELLOW_3:46; suppose D = {}; then sup D = Bottom [:S,T:] & sup proj1 D = Bottom S & sup proj2 D = Bottom T by FUNCT_5:10,YELLOW_0:def 11; hence [sup proj1 D,sup proj2 D] = sup D by Th4; end; theorem for S, T being upper-bounded antisymmetric (non empty RelStr), D being Subset of [:S,T:] st [:S,T:] is complete or ex_inf_of D,[:S,T:] holds inf D = [inf proj1 D,inf proj2 D] proof let S, T be upper-bounded antisymmetric non empty RelStr, D be Subset of [:S,T:] such that A1: [:S,T:] is complete or ex_inf_of D,[:S,T:]; per cases; suppose D <> {}; hence thesis by A1,YELLOW_3:47; suppose D = {}; then inf D = Top [:S,T:] & inf proj1 D = Top S & inf proj2 D = Top T by FUNCT_5:10,YELLOW_0:def 12; hence [inf proj1 D,inf proj2 D] = inf D by Th3; end; theorem for S, T being non empty RelStr, x, y being Element of [:S,T:] holds x is_<=_than {y} iff x`1 is_<=_than {y`1} & x`2 is_<=_than {y`2} proof let S, T be non empty RelStr, x, y be Element of [:S,T:]; thus x is_<=_than {y} implies x`1 is_<=_than {y`1} & x`2 is_<=_than {y`2} proof assume A1: for b being Element of [:S,T:] st b in {y} holds x <= b; A2: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; then y = [y`1,y`2] by MCART_1:23; then [y`1,y`2] in {y} by TARSKI:def 1; then A3: x <= [y`1,y`2] by A1; A4: x = [x`1,x`2] by A2,MCART_1:23; hereby let b be Element of S; assume b in {y`1}; then b = y`1 by TARSKI:def 1; hence x`1 <= b by A3,A4,YELLOW_3:11; end; let b be Element of T; assume b in {y`2}; then b = y`2 by TARSKI:def 1; hence x`2 <= b by A3,A4,YELLOW_3:11; end; assume that A5: for b being Element of S st b in {y`1} holds x`1 <= b and A6: for b being Element of T st b in {y`2} holds x`2 <= b; let b be Element of [:S,T:]; assume b in {y}; then b = y by TARSKI:def 1; then b`1 in {y`1} & b`2 in {y`2} by TARSKI:def 1; then x`1 <= b`1 & x`2 <= b`2 by A5,A6; hence x <= b by YELLOW_3:12; end; theorem for S, T being non empty RelStr, x, y, z being Element of [:S,T:] holds x is_<=_than {y,z} iff x`1 is_<=_than {y`1,z`1} & x`2 is_<=_than {y`2,z`2} proof let S, T be non empty RelStr, x, y, z be Element of [:S,T:]; thus x is_<=_than {y,z} implies x`1 is_<=_than {y`1,z`1} & x`2 is_<=_than {y`2,z`2} proof assume A1: for b being Element of [:S,T:] st b in {y,z} holds x <= b; A2: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; then y = [y`1,y`2] & z = [z`1,z`2] by MCART_1:23; then [y`1,y`2] in {y,z} & [z`1,z`2] in {y,z} by TARSKI:def 2; then A3: x <= [y`1,y`2] & x <= [z`1,z`2] by A1; A4: x = [x`1,x`2] by A2,MCART_1:23; hereby let b be Element of S; assume b in {y`1,z`1}; then b = y`1 or b = z`1 by TARSKI:def 2; hence x`1 <= b by A3,A4,YELLOW_3:11; end; let b be Element of T; assume b in {y`2,z`2}; then b = y`2 or b = z`2 by TARSKI:def 2; hence x`2 <= b by A3,A4,YELLOW_3:11; end; assume that A5: for b being Element of S st b in {y`1,z`1} holds x`1 <= b and A6: for b being Element of T st b in {y`2,z`2} holds x`2 <= b; let b be Element of [:S,T:]; assume b in {y,z}; then b = y or b = z by TARSKI:def 2; then b`1 in {y`1,z`1} & b`2 in {y`2,z`2} by TARSKI:def 2; then x`1 <= b`1 & x`2 <= b`2 by A5,A6; hence x <= b by YELLOW_3:12; end; theorem for S, T being non empty RelStr, x, y being Element of [:S,T:] holds x is_>=_than {y} iff x`1 is_>=_than {y`1} & x`2 is_>=_than {y`2} proof let S, T be non empty RelStr, x, y be Element of [:S,T:]; thus x is_>=_than {y} implies x`1 is_>=_than {y`1} & x`2 is_>=_than {y`2} proof assume A1: for b being Element of [:S,T:] st b in {y} holds x >= b; A2: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; then y = [y`1,y`2] by MCART_1:23; then [y`1,y`2] in {y} by TARSKI:def 1; then A3: x >= [y`1,y`2] by A1; A4: x = [x`1,x`2] by A2,MCART_1:23; hereby let b be Element of S; assume b in {y`1}; then b = y`1 by TARSKI:def 1; hence x`1 >= b by A3,A4,YELLOW_3:11; end; let b be Element of T; assume b in {y`2}; then b = y`2 by TARSKI:def 1; hence x`2 >= b by A3,A4,YELLOW_3:11; end; assume that A5: for b being Element of S st b in {y`1} holds x`1 >= b and A6: for b being Element of T st b in {y`2} holds x`2 >= b; let b be Element of [:S,T:]; assume b in {y}; then b = y by TARSKI:def 1; then b`1 in {y`1} & b`2 in {y`2} by TARSKI:def 1; then x`1 >= b`1 & x`2 >= b`2 by A5,A6; hence x >= b by YELLOW_3:12; end; theorem for S, T being non empty RelStr, x, y, z being Element of [:S,T:] holds x is_>=_than {y,z} iff x`1 is_>=_than {y`1,z`1} & x`2 is_>=_than {y`2,z`2} proof let S, T be non empty RelStr, x, y, z be Element of [:S,T:]; thus x is_>=_than {y,z} implies x`1 is_>=_than {y`1,z`1} & x`2 is_>=_than {y`2,z`2} proof assume A1: for b being Element of [:S,T:] st b in {y,z} holds x >= b; A2: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; then y = [y`1,y`2] & z = [z`1,z`2] by MCART_1:23; then [y`1,y`2] in {y,z} & [z`1,z`2] in {y,z} by TARSKI:def 2; then A3: x >= [y`1,y`2] & x >= [z`1,z`2] by A1; A4: x = [x`1,x`2] by A2,MCART_1:23; hereby let b be Element of S; assume b in {y`1,z`1}; then b = y`1 or b = z`1 by TARSKI:def 2; hence x`1 >= b by A3,A4,YELLOW_3:11; end; let b be Element of T; assume b in {y`2,z`2}; then b = y`2 or b = z`2 by TARSKI:def 2; hence x`2 >= b by A3,A4,YELLOW_3:11; end; assume that A5: for b being Element of S st b in {y`1,z`1} holds x`1 >= b and A6: for b being Element of T st b in {y`2,z`2} holds x`2 >= b; let b be Element of [:S,T:]; assume b in {y,z}; then b = y or b = z by TARSKI:def 2; then b`1 in {y`1,z`1} & b`2 in {y`2,z`2} by TARSKI:def 2; then x`1 >= b`1 & x`2 >= b`2 by A5,A6; hence x >= b by YELLOW_3:12; end; theorem for S, T being non empty antisymmetric RelStr, x, y being Element of [:S,T:] holds ex_inf_of {x,y},[:S,T:] iff ex_inf_of {x`1,y`1}, S & ex_inf_of {x`2,y`2}, T proof let S, T be non empty antisymmetric RelStr, x, y be Element of [:S,T:]; the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; then x = [x`1,x`2] & y = [y`1,y`2] by MCART_1:23; then proj1 {x,y} = {x`1,y`1} & proj2 {x,y} = {x`2,y`2} by FUNCT_5:16; hence thesis by YELLOW_3:42; end; theorem for S, T being non empty antisymmetric RelStr, x, y being Element of [:S,T:] holds ex_sup_of {x,y},[:S,T:] iff ex_sup_of {x`1,y`1}, S & ex_sup_of {x`2,y`2}, T proof let S, T be non empty antisymmetric RelStr, x, y be Element of [:S,T:]; the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; then x = [x`1,x`2] & y = [y`1,y`2] by MCART_1:23; then proj1 {x,y} = {x`1,y`1} & proj2 {x,y} = {x`2,y`2} by FUNCT_5:16; hence thesis by YELLOW_3:41; end; theorem Th13: for S, T being with_infima antisymmetric RelStr, x, y being Element of [:S,T:] holds (x "/\" y)`1 = x`1 "/\" y`1 & (x "/\" y)`2 = x`2 "/\" y`2 proof let S, T be with_infima antisymmetric RelStr, x, y be Element of [:S,T:]; the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; then A1: x = [x`1,x`2] & y = [y`1,y`2] by MCART_1:23; set a = (x "/\" y)`1, b = (x "/\" y)`2; x "/\" y <= x & x "/\" y <= y by YELLOW_0:23; then A2: a <= x`1 & a <= y`1 & b <= x`2 & b <= y`2 by YELLOW_3:12; A3: for d being Element of S st d <= x`1 & d <= y`1 holds a >= d proof let d be Element of S such that A4: d <= x`1 & d <= y`1; set t = x`2 "/\" y`2; t <= x`2 & t <= y`2 by YELLOW_0:23; then [d,t] <= x & [d,t] <= y by A1,A4,YELLOW_3:11; then A5: x "/\" y >= [d,t] by YELLOW_0:23; [d,t]`1 = d by MCART_1:7; hence a >= d by A5,YELLOW_3:12; end; for d being Element of T st d <= x`2 & d <= y`2 holds b >= d proof let d be Element of T such that A6: d <= x`2 & d <= y`2; set s = x`1 "/\" y`1; s <= x`1 & s <= y`1 by YELLOW_0:23; then [s,d] <= x & [s,d] <= y by A1,A6,YELLOW_3:11; then A7: x "/\" y >= [s,d] by YELLOW_0:23; [s,d]`2 = d by MCART_1:7; hence b >= d by A7,YELLOW_3:12; end; hence thesis by A2,A3,YELLOW_0:19; end; theorem Th14: for S, T being with_suprema antisymmetric RelStr, x, y being Element of [:S,T:] holds (x "\/" y)`1 = x`1 "\/" y`1 & (x "\/" y)`2 = x`2 "\/" y`2 proof let S, T be with_suprema antisymmetric RelStr, x, y be Element of [:S,T:]; the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; then A1: x = [x`1,x`2] & y = [y`1,y`2] by MCART_1:23; set a = (x "\/" y)`1, b = (x "\/" y)`2; x "\/" y >= x & x "\/" y >= y by YELLOW_0:22; then A2: a >= x`1 & a >= y`1 & b >= x`2 & b >= y`2 by YELLOW_3:12; A3: for d being Element of S st d >= x`1 & d >= y`1 holds a <= d proof let d be Element of S such that A4: d >= x`1 & d >= y`1; set t = x`2 "\/" y`2; t >= x`2 & t >= y`2 by YELLOW_0:22; then [d,t] >= x & [d,t] >= y by A1,A4,YELLOW_3:11; then A5: x "\/" y <= [d,t] by YELLOW_0:22; [d,t]`1 = d by MCART_1:7; hence a <= d by A5,YELLOW_3:12; end; for d being Element of T st d >= x`2 & d >= y`2 holds b <= d proof let d be Element of T such that A6: d >= x`2 & d >= y`2; set s = x`1 "\/" y`1; s >= x`1 & s >= y`1 by YELLOW_0:22; then [s,d] >= x & [s,d] >= y by A1,A6,YELLOW_3:11; then A7: x "\/" y <= [s,d] by YELLOW_0:22; [s,d]`2 = d by MCART_1:7; hence b <= d by A7,YELLOW_3:12; end; hence thesis by A2,A3,YELLOW_0:18; end; theorem Th15: for S, T being with_infima antisymmetric RelStr, x1, y1 being Element of S, x2, y2 being Element of T holds [x1 "/\" y1, x2 "/\" y2] = [x1,x2] "/\" [y1,y2] proof let S, T be with_infima antisymmetric RelStr, x1, y1 be Element of S, x2, y2 be Element of T; A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; A2: ([x1,x2] "/\" [y1,y2])`1 = [x1,x2]`1 "/\" [y1,y2]`1 by Th13 .= x1 "/\" [y1,y2]`1 by MCART_1:7 .= x1 "/\" y1 by MCART_1:7 .= [x1 "/\" y1, x2 "/\" y2]`1 by MCART_1:7; ([x1,x2] "/\" [y1,y2])`2 = [x1,x2]`2 "/\" [y1,y2]`2 by Th13 .= x2 "/\" [y1,y2]`2 by MCART_1:7 .= x2 "/\" y2 by MCART_1:7 .= [x1 "/\" y1, x2 "/\" y2]`2 by MCART_1:7; hence thesis by A1,A2,DOMAIN_1:12; end; theorem Th16: for S, T being with_suprema antisymmetric RelStr, x1, y1 being Element of S, x2, y2 being Element of T holds [x1 "\/" y1, x2 "\/" y2] = [x1,x2] "\/" [y1,y2] proof let S, T be with_suprema antisymmetric RelStr, x1, y1 be Element of S, x2, y2 be Element of T; A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; A2: ([x1,x2] "\/" [y1,y2])`1 = [x1,x2]`1 "\/" [y1,y2]`1 by Th14 .= x1 "\/" [y1,y2]`1 by MCART_1:7 .= x1 "\/" y1 by MCART_1:7 .= [x1 "\/" y1, x2 "\/" y2]`1 by MCART_1:7; ([x1,x2] "\/" [y1,y2])`2 = [x1,x2]`2 "\/" [y1,y2]`2 by Th14 .= x2 "\/" [y1,y2]`2 by MCART_1:7 .= x2 "\/" y2 by MCART_1:7 .= [x1 "\/" y1, x2 "\/" y2]`2 by MCART_1:7; hence thesis by A1,A2,DOMAIN_1:12; end; definition let S be with_suprema with_infima antisymmetric RelStr, x, y be Element of S; redefine pred y is_a_complement_of x; symmetry proof let a, b be Element of S; assume a is_a_complement_of b; hence a "\/" b = Top S & a "/\" b = Bottom S by WAYBEL_1:def 23; end; end; theorem Th17: for S, T being bounded with_suprema with_infima antisymmetric RelStr, x, y being Element of [:S,T:] holds x is_a_complement_of y iff x`1 is_a_complement_of y`1 & x`2 is_a_complement_of y`2 proof let S, T be bounded with_suprema with_infima antisymmetric RelStr, x, y be Element of [:S,T:]; hereby assume A1: x is_a_complement_of y; thus x`1 is_a_complement_of y`1 proof thus y`1 "\/" x`1 = (y "\/" x)`1 by Th14 .= (Top [:S,T:])`1 by A1,WAYBEL_1:def 23 .= [Top S,Top T]`1 by Th3 .= Top S by MCART_1:7; thus y`1 "/\" x`1 = (y "/\" x)`1 by Th13 .= (Bottom [:S,T:])`1 by A1,WAYBEL_1:def 23 .= [Bottom S,Bottom T]`1 by Th4 .= Bottom S by MCART_1:7; end; thus x`2 is_a_complement_of y`2 proof thus y`2 "\/" x`2 = (y "\/" x)`2 by Th14 .= (Top [:S,T:])`2 by A1,WAYBEL_1:def 23 .= [Top S,Top T]`2 by Th3 .= Top T by MCART_1:7; thus y`2 "/\" x`2 = (y "/\" x)`2 by Th13 .= (Bottom [:S,T:])`2 by A1,WAYBEL_1:def 23 .= [Bottom S,Bottom T]`2 by Th4 .= Bottom T by MCART_1:7; end; end; A2: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; assume that A3: y`1 "\/" x`1 = Top S and A4: y`1 "/\" x`1 = Bottom S and A5: y`2 "\/" x`2 = Top T and A6: y`2 "/\" x`2 = Bottom T; A7: (y "\/" x)`1 = y`1 "\/" x`1 by Th14 .= [Top S,Top T]`1 by A3,MCART_1:7; (y "\/" x)`2 = y`2 "\/" x`2 by Th14 .= [Top S,Top T]`2 by A5,MCART_1:7; hence y "\/" x = [Top S,Top T] by A2,A7,DOMAIN_1:12 .= Top [:S,T:] by Th3; A8: (y "/\" x)`1 = y`1 "/\" x`1 by Th13 .= [Bottom S,Bottom T]`1 by A4,MCART_1:7; (y "/\" x)`2 = y`2 "/\" x`2 by Th13 .= [Bottom S,Bottom T]`2 by A6,MCART_1:7; hence y "/\" x = [Bottom S,Bottom T] by A2,A8,DOMAIN_1:12 .= Bottom [:S,T:] by Th4; end; theorem Th18: for S, T being antisymmetric up-complete (non empty reflexive RelStr), a, c being Element of S, b, d being Element of T st [a,b] << [c,d] holds a << c & b << d proof let S, T be antisymmetric up-complete (non empty reflexive RelStr), a, c be Element of S, b, d be Element of T; A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; assume A2: for D being non empty directed Subset of [:S,T:] st [c,d] <= sup D ex e being Element of [:S,T:] st e in D & [a,b] <= e; thus a << c proof let D be non empty directed Subset of S such that A3: c <= sup D; reconsider d' = {d} as non empty directed Subset of T by WAYBEL_0:5; ex_sup_of D,S & ex_sup_of d',T by WAYBEL_0:75; then A4: sup [:D,d':] = [sup D,sup d'] by YELLOW_3:43; d <= sup d' by YELLOW_0:39; then [c,d] <= sup [:D,d':] by A3,A4,YELLOW_3:11; then consider e being Element of [:S,T:] such that A5: e in [:D,d':] & [a,b] <= e by A2; take e`1; thus e`1 in D by A5,MCART_1:10; e = [e`1,e`2] by A1,MCART_1:23; hence a <= e`1 by A5,YELLOW_3:11; end; let D be non empty directed Subset of T such that A6: d <= sup D; reconsider c' = {c} as non empty directed Subset of S by WAYBEL_0:5; ex_sup_of c',S & ex_sup_of D,T by WAYBEL_0:75; then A7: sup [:c',D:] = [sup c',sup D] by YELLOW_3:43; c <= sup c' by YELLOW_0:39; then [c,d] <= sup [:c',D:] by A6,A7,YELLOW_3:11; then consider e being Element of [:S,T:] such that A8: e in [:c',D:] & [a,b] <= e by A2; take e`2; thus e`2 in D by A8,MCART_1:10; e = [e`1,e`2] by A1,MCART_1:23; hence b <= e`2 by A8,YELLOW_3:11; end; theorem Th19: for S, T being up-complete (non empty Poset) for a, c being Element of S, b, d being Element of T holds [a,b] << [c,d] iff a << c & b << d proof let S, T be up-complete (non empty Poset), a, c be Element of S, b, d be Element of T; thus [a,b] << [c,d] implies a << c & b << d by Th18; A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; assume A2: for D being non empty directed Subset of S st c <= sup D ex e being Element of S st e in D & a <= e; assume A3: for D being non empty directed Subset of T st d <= sup D ex e being Element of T st e in D & b <= e; let D be non empty directed Subset of [:S,T:] such that A4: [c,d] <= sup D; A5: proj1 D is non empty directed & proj2 D is non empty directed by YELLOW_3:21,22; ex_sup_of D,[:S,T:] by WAYBEL_0:75; then A6: sup D = [sup proj1 D,sup proj2 D] by YELLOW_3:46; then c <= sup proj1 D by A4,YELLOW_3:11; then consider e being Element of S such that A7: e in proj1 D & a <= e by A2,A5; d <= sup proj2 D by A4,A6,YELLOW_3:11; then consider f being Element of T such that A8: f in proj2 D & b <= f by A3,A5; consider e2 being set such that A9: [e,e2] in D by A7,FUNCT_5:def 1; consider f1 being set such that A10: [f1,f] in D by A8,FUNCT_5:def 2; e2 in the carrier of T by A1,A9,ZFMISC_1:106; then reconsider e2 as Element of T; f1 in the carrier of S by A1,A10,ZFMISC_1:106; then reconsider f1 as Element of S; consider ef being Element of [:S,T:] such that A11: ef in D & [e,e2] <= ef & [f1,f] <= ef by A9,A10,WAYBEL_0:def 1; take ef; thus ef in D by A11; A12: [a,b] <= [e,f] by A7,A8,YELLOW_3:11; A13: ef = [ef`1,ef`2] by A1,MCART_1:23; then e <= ef`1 & f <= ef`2 by A11,YELLOW_3:11; then [e,f] <= ef by A13,YELLOW_3:11; hence [a,b] <= ef by A12,ORDERS_1:26; end; theorem Th20: for S, T being antisymmetric up-complete (non empty reflexive RelStr), x, y being Element of [:S,T:] st x << y holds x`1 << y`1 & x`2 << y`2 proof let S, T be antisymmetric up-complete (non empty reflexive RelStr), x, y be Element of [:S,T:] such that A1: x << y; the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; then x = [x`1,x`2] & y = [y`1,y`2] by MCART_1:23; hence x`1 << y`1 & x`2 << y`2 by A1,Th18; end; theorem Th21: for S, T being up-complete (non empty Poset), x, y being Element of [:S,T:] holds x << y iff x`1 << y`1 & x`2 << y`2 proof let S, T be up-complete (non empty Poset), x, y be Element of [:S,T:]; the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; then x = [x`1,x`2] & y = [y`1,y`2] by MCART_1:23; hence thesis by Th19; end; theorem Th22: for S, T being antisymmetric up-complete (non empty reflexive RelStr), x being Element of [:S,T:] st x is compact holds x`1 is compact & x`2 is compact proof let S, T be antisymmetric up-complete (non empty reflexive RelStr), x be Element of [:S,T:]; assume A1: x << x; hence x`1 << x`1 by Th20; thus x`2 << x`2 by A1,Th20; end; theorem Th23: for S, T being up-complete (non empty Poset), x being Element of [:S,T:] st x`1 is compact & x`2 is compact holds x is compact proof let S, T be up-complete (non empty Poset), x be Element of [:S,T:]; assume x`1 << x`1 & x`2 << x`2; hence x << x by Th21; end; begin :: On the subsets of product of relational structures theorem Th24: for S, T being with_infima antisymmetric RelStr, X, Y being Subset of [:S,T:] holds proj1 (X "/\" Y) = proj1 X "/\" proj1 Y & proj2 (X "/\" Y) = proj2 X "/\" proj2 Y proof let S, T be with_infima antisymmetric RelStr, X, Y be Subset of [:S,T:]; A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; A2: X "/\" Y = { x "/\" y where x, y is Element of [:S,T:]: x in X & y in Y } by YELLOW_4:def 4; A3: proj1 X "/\" proj1 Y = { x "/\" y where x, y is Element of S: x in proj1 X & y in proj1 Y } by YELLOW_4:def 4; hereby hereby let a be set; assume a in proj1 (X "/\" Y); then consider b being set such that A4: [a,b] in X "/\" Y by FUNCT_5:def 1; consider x, y being Element of [:S,T:] such that A5: [a,b] = x "/\" y and A6: x in X & y in Y by A2,A4; A7: a = [a,b]`1 by MCART_1:7 .= x`1 "/\" y`1 by A5,Th13; x = [x`1,x`2] & y = [y`1,y`2] by A1,MCART_1:23; then x`1 in proj1 X & y`1 in proj1 Y by A6,FUNCT_5:4; hence a in proj1 X "/\" proj1 Y by A7,YELLOW_4:37; end; let a be set; assume a in proj1 X "/\" proj1 Y; then consider x, y being Element of S such that A8: a = x "/\" y & x in proj1 X & y in proj1 Y by A3; consider x2 being set such that A9: [x,x2] in X by A8,FUNCT_5:def 1; consider y2 being set such that A10: [y,y2] in Y by A8,FUNCT_5:def 1; x2 in the carrier of T & y2 in the carrier of T by A1,A9,A10,ZFMISC_1:106; then reconsider x2, y2 as Element of T; [x,x2] "/\" [y,y2] = [a,x2 "/\" y2] by A8,Th15; then [a,x2 "/\" y2] in X "/\" Y by A9,A10,YELLOW_4:37; hence a in proj1 (X "/\" Y) by FUNCT_5:def 1; end; A11: proj2 X "/\" proj2 Y = { x "/\" y where x, y is Element of T: x in proj2 X & y in proj2 Y } by YELLOW_4:def 4; hereby let b be set; assume b in proj2 (X "/\" Y); then consider a being set such that A12: [a,b] in X "/\" Y by FUNCT_5:def 2; consider x, y being Element of [:S,T:] such that A13: [a,b] = x "/\" y and A14: x in X & y in Y by A2,A12; A15: b = [a,b]`2 by MCART_1:7 .= x`2 "/\" y`2 by A13,Th13; x = [x`1,x`2] & y = [y`1,y`2] by A1,MCART_1:23; then x`2 in proj2 X & y`2 in proj2 Y by A14,FUNCT_5:4; hence b in proj2 X "/\" proj2 Y by A15,YELLOW_4:37; end; let b be set; assume b in proj2 X "/\" proj2 Y; then consider x, y being Element of T such that A16: b = x "/\" y & x in proj2 X & y in proj2 Y by A11; consider x1 being set such that A17: [x1,x] in X by A16,FUNCT_5:def 2; consider y1 being set such that A18: [y1,y] in Y by A16,FUNCT_5:def 2; x1 in the carrier of S & y1 in the carrier of S by A1,A17,A18,ZFMISC_1:106; then reconsider x1, y1 as Element of S; [x1,x] "/\" [y1,y] = [x1 "/\" y1,b] by A16,Th15; then [x1 "/\" y1,b] in X "/\" Y by A17,A18,YELLOW_4:37; hence b in proj2 (X "/\" Y) by FUNCT_5:def 2; end; theorem for S, T being with_suprema antisymmetric RelStr, X, Y being Subset of [:S,T:] holds proj1 (X "\/" Y) = proj1 X "\/" proj1 Y & proj2 (X "\/" Y) = proj2 X "\/" proj2 Y proof let S, T be with_suprema antisymmetric RelStr, X, Y be Subset of [:S,T:]; A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; A2: X "\/" Y = { x "\/" y where x, y is Element of [:S,T:]: x in X & y in Y } by YELLOW_4:def 3; A3: proj1 X "\/" proj1 Y = { x "\/" y where x, y is Element of S: x in proj1 X & y in proj1 Y } by YELLOW_4:def 3; hereby hereby let a be set; assume a in proj1 (X "\/" Y); then consider b being set such that A4: [a,b] in X "\/" Y by FUNCT_5:def 1; consider x, y being Element of [:S,T:] such that A5: [a,b] = x "\/" y and A6: x in X & y in Y by A2,A4; A7: a = [a,b]`1 by MCART_1:7 .= x`1 "\/" y`1 by A5,Th14; x = [x`1,x`2] & y = [y`1,y`2] by A1,MCART_1:23; then x`1 in proj1 X & y`1 in proj1 Y by A6,FUNCT_5:4; hence a in proj1 X "\/" proj1 Y by A7,YELLOW_4:10; end; let a be set; assume a in proj1 X "\/" proj1 Y; then consider x, y being Element of S such that A8: a = x "\/" y & x in proj1 X & y in proj1 Y by A3; consider x2 being set such that A9: [x,x2] in X by A8,FUNCT_5:def 1; consider y2 being set such that A10: [y,y2] in Y by A8,FUNCT_5:def 1; x2 in the carrier of T & y2 in the carrier of T by A1,A9,A10,ZFMISC_1:106; then reconsider x2, y2 as Element of T; [x,x2] "\/" [y,y2] = [a,x2 "\/" y2] by A8,Th16; then [a,x2 "\/" y2] in X "\/" Y by A9,A10,YELLOW_4:10; hence a in proj1 (X "\/" Y) by FUNCT_5:def 1; end; A11: proj2 X "\/" proj2 Y = { x "\/" y where x, y is Element of T: x in proj2 X & y in proj2 Y } by YELLOW_4:def 3; hereby let b be set; assume b in proj2 (X "\/" Y); then consider a being set such that A12: [a,b] in X "\/" Y by FUNCT_5:def 2; consider x, y being Element of [:S,T:] such that A13: [a,b] = x "\/" y and A14: x in X & y in Y by A2,A12; A15: b = [a,b]`2 by MCART_1:7 .= x`2 "\/" y`2 by A13,Th14; x = [x`1,x`2] & y = [y`1,y`2] by A1,MCART_1:23; then x`2 in proj2 X & y`2 in proj2 Y by A14,FUNCT_5:4; hence b in proj2 X "\/" proj2 Y by A15,YELLOW_4:10; end; let b be set; assume b in proj2 X "\/" proj2 Y; then consider x, y being Element of T such that A16: b = x "\/" y & x in proj2 X & y in proj2 Y by A11; consider x1 being set such that A17: [x1,x] in X by A16,FUNCT_5:def 2; consider y1 being set such that A18: [y1,y] in Y by A16,FUNCT_5:def 2; x1 in the carrier of S & y1 in the carrier of S by A1,A17,A18,ZFMISC_1:106; then reconsider x1, y1 as Element of S; [x1,x] "\/" [y1,y] = [x1 "\/" y1,b] by A16,Th16; then [x1 "\/" y1,b] in X "\/" Y by A17,A18,YELLOW_4:10; hence b in proj2 (X "\/" Y) by FUNCT_5:def 2; end; theorem for S, T being RelStr, X being Subset of [:S,T:] holds downarrow X c= [:downarrow proj1 X,downarrow proj2 X:] proof let S, T be RelStr, X be Subset of [:S,T:]; A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; let x be set; assume A2: x in downarrow X; then consider a, b being set such that A3: a in the carrier of S & b in the carrier of T and x = [a,b] by A1,ZFMISC_1:def 2; reconsider S' = S, T' = T as non empty RelStr by A3,STRUCT_0:def 1; reconsider x' = x as Element of [:S',T':] by A2; consider y being Element of [:S',T':] such that A4: y >= x' & y in X by A2,WAYBEL_0:def 15; A5: y`1 >= x'`1 & y`2 >= x'`2 by A4,YELLOW_3:12; y = [y`1,y`2] by A1,MCART_1:23; then y`1 in proj1 X & y`2 in proj2 X by A4,FUNCT_5:4; then A6: x`1 in downarrow proj1 X & x`2 in downarrow proj2 X by A5,WAYBEL_0:def 15; x' = [x'`1,x'`2] by A1,MCART_1:23; hence x in [:downarrow proj1 X,downarrow proj2 X:] by A6,MCART_1:11; end; theorem for S, T being RelStr, X being Subset of S, Y being Subset of T holds [:downarrow X,downarrow Y:] = downarrow [:X,Y:] proof let S, T be RelStr, X be Subset of S, Y be Subset of T; A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; hereby let x be set; assume x in [:downarrow X,downarrow Y:]; then consider x1, x2 being set such that A2: x1 in downarrow X & x2 in downarrow Y & x = [x1,x2] by ZFMISC_1:def 2; reconsider S' = S, T' = T as non empty RelStr by A2,STRUCT_0:def 1; reconsider x1 as Element of S' by A2; reconsider x2 as Element of T' by A2; consider y1 being Element of S' such that A3: y1 >= x1 & y1 in X by A2,WAYBEL_0:def 15; consider y2 being Element of T' such that A4: y2 >= x2 & y2 in Y by A2,WAYBEL_0:def 15; A5: [y1,y2] in [:X,Y:] by A3,A4,ZFMISC_1:106; [y1,y2] >= [x1,x2] by A3,A4,YELLOW_3:11; hence x in downarrow [:X,Y:] by A2,A5,WAYBEL_0:def 15; end; let x be set; assume A6: x in downarrow [:X,Y:]; then consider a, b being set such that A7: a in the carrier of S & b in the carrier of T and x = [a,b] by A1,ZFMISC_1:def 2; reconsider S' = S, T' = T as non empty RelStr by A7,STRUCT_0:def 1; reconsider x' = x as Element of [:S',T':] by A6; consider y being Element of [:S',T':] such that A8: y >= x' & y in [:X,Y:] by A6,WAYBEL_0:def 15; A9: y`1 >= x'`1 & y`2 >= x'`2 by A8,YELLOW_3:12; y`1 in X & y`2 in Y by A8,MCART_1:10; then A10: x`1 in downarrow X & x`2 in downarrow Y by A9,WAYBEL_0:def 15; x' = [x'`1,x'`2] by A1,MCART_1:23; hence x in [:downarrow X,downarrow Y:] by A10,MCART_1:11; end; theorem Th28: for S, T being RelStr, X being Subset of [:S,T:] holds proj1 downarrow X c= downarrow proj1 X & proj2 downarrow X c= downarrow proj2 X proof let S, T be RelStr, X be Subset of [:S,T:]; A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; hereby let a be set; assume a in proj1 downarrow X; then consider b being set such that A2: [a,b] in downarrow X by FUNCT_5:def 1; A3: a in the carrier of S & b in the carrier of T by A1,A2,ZFMISC_1:106; then reconsider S' = S, T' = T as non empty RelStr by STRUCT_0:def 1; reconsider a' = a as Element of S' by A3; reconsider b' = b as Element of T' by A3; consider c being Element of [:S',T':] such that A4: [a',b'] <= c & c in X by A2,WAYBEL_0:def 15; A5: c = [c`1,c`2] by A1,MCART_1:23; then A6: a' <= c`1 by A4,YELLOW_3:11; c`1 in proj1 X by A4,A5,FUNCT_5:4; hence a in downarrow proj1 X by A6,WAYBEL_0:def 15; end; let b be set; assume b in proj2 downarrow X; then consider a being set such that A7: [a,b] in downarrow X by FUNCT_5:def 2; A8: a in the carrier of S & b in the carrier of T by A1,A7,ZFMISC_1:106; then reconsider S' = S, T' = T as non empty RelStr by STRUCT_0:def 1; reconsider a' = a as Element of S' by A8; reconsider b' = b as Element of T' by A8; consider c being Element of [:S',T':] such that A9: [a',b'] <= c & c in X by A7,WAYBEL_0:def 15; A10: c = [c`1,c`2] by A1,MCART_1:23; then A11: b' <= c`2 by A9,YELLOW_3:11; c`2 in proj2 X by A9,A10,FUNCT_5:4; hence b in downarrow proj2 X by A11,WAYBEL_0:def 15; end; theorem for S being RelStr, T being reflexive RelStr, X being Subset of [:S,T:] holds proj1 downarrow X = downarrow proj1 X proof let S be RelStr, T be reflexive RelStr, X be Subset of [:S,T:]; A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; thus proj1 downarrow X c= downarrow proj1 X by Th28; let a be set; assume A2: a in downarrow proj1 X; then reconsider S' = S as non empty RelStr by STRUCT_0:def 1; reconsider a' = a as Element of S' by A2; consider b being Element of S' such that A3: b >= a' & b in proj1 X by A2,WAYBEL_0:def 15; consider b2 being set such that A4: [b,b2] in X by A3,FUNCT_5:def 1; A5: b2 in the carrier of T by A1,A4,ZFMISC_1:106; then reconsider T' = T as non empty reflexive RelStr by STRUCT_0:def 1; reconsider b2 as Element of T' by A5; b2 <= b2; then [b,b2] >= [a',b2] by A3,YELLOW_3:11; then [a',b2] in downarrow X by A4,WAYBEL_0:def 15; hence a in proj1 downarrow X by FUNCT_5:def 1; end; theorem for S being reflexive RelStr, T being RelStr, X being Subset of [:S,T:] holds proj2 downarrow X = downarrow proj2 X proof let S be reflexive RelStr, T be RelStr, X be Subset of [:S,T:]; A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; thus proj2 downarrow X c= downarrow proj2 X by Th28; let c be set; assume A2: c in downarrow proj2 X; then reconsider T' = T as non empty RelStr by STRUCT_0:def 1; reconsider c' = c as Element of T' by A2; consider b being Element of T' such that A3: b >= c' & b in proj2 X by A2,WAYBEL_0:def 15; consider b1 being set such that A4: [b1,b] in X by A3,FUNCT_5:def 2; A5: b1 in the carrier of S by A1,A4,ZFMISC_1:106; then reconsider S' = S as non empty reflexive RelStr by STRUCT_0:def 1; reconsider b1 as Element of S' by A5; b1 <= b1; then [b1,b] >= [b1,c'] by A3,YELLOW_3:11; then [b1,c'] in downarrow X by A4,WAYBEL_0:def 15; hence c in proj2 downarrow X by FUNCT_5:def 2; end; theorem for S, T being RelStr, X being Subset of [:S,T:] holds uparrow X c= [:uparrow proj1 X,uparrow proj2 X:] proof let S, T be RelStr, X be Subset of [:S,T:]; A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; let x be set; assume A2: x in uparrow X; then consider a, b being set such that A3: a in the carrier of S & b in the carrier of T and x = [a,b] by A1,ZFMISC_1:def 2; reconsider S' = S, T' = T as non empty RelStr by A3,STRUCT_0:def 1; reconsider x' = x as Element of [:S',T':] by A2; consider y being Element of [:S',T':] such that A4: y <= x' & y in X by A2,WAYBEL_0:def 16; A5: y`1 <= x'`1 & y`2 <= x'`2 by A4,YELLOW_3:12; y = [y`1,y`2] by A1,MCART_1:23; then y`1 in proj1 X & y`2 in proj2 X by A4,FUNCT_5:4; then A6: x`1 in uparrow proj1 X & x`2 in uparrow proj2 X by A5,WAYBEL_0:def 16; x' = [x'`1,x'`2] by A1,MCART_1:23; hence x in [:uparrow proj1 X,uparrow proj2 X:] by A6,MCART_1:11; end; theorem for S, T being RelStr, X being Subset of S, Y being Subset of T holds [:uparrow X,uparrow Y:] = uparrow [:X,Y:] proof let S, T be RelStr, X be Subset of S, Y be Subset of T; A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; hereby let x be set; assume x in [:uparrow X,uparrow Y:]; then consider x1, x2 being set such that A2: x1 in uparrow X & x2 in uparrow Y & x = [x1,x2] by ZFMISC_1:def 2; reconsider S' = S, T' = T as non empty RelStr by A2,STRUCT_0:def 1; reconsider x1 as Element of S' by A2; reconsider x2 as Element of T' by A2; consider y1 being Element of S' such that A3: y1 <= x1 & y1 in X by A2,WAYBEL_0:def 16; consider y2 being Element of T' such that A4: y2 <= x2 & y2 in Y by A2,WAYBEL_0:def 16; A5: [y1,y2] in [:X,Y:] by A3,A4,ZFMISC_1:106; [y1,y2] <= [x1,x2] by A3,A4,YELLOW_3:11; hence x in uparrow [:X,Y:] by A2,A5,WAYBEL_0:def 16; end; let x be set; assume A6: x in uparrow [:X,Y:]; then consider a, b being set such that A7: a in the carrier of S & b in the carrier of T and x = [a,b] by A1,ZFMISC_1:def 2; reconsider S' = S, T' = T as non empty RelStr by A7,STRUCT_0:def 1; reconsider x' = x as Element of [:S',T':] by A6; consider y being Element of [:S',T':] such that A8: y <= x' & y in [:X,Y:] by A6,WAYBEL_0:def 16; A9: y`1 <= x'`1 & y`2 <= x'`2 by A8,YELLOW_3:12; y`1 in X & y`2 in Y by A8,MCART_1:10; then A10: x`1 in uparrow X & x`2 in uparrow Y by A9,WAYBEL_0:def 16; x' = [x'`1,x'`2] by A1,MCART_1:23; hence x in [:uparrow X,uparrow Y:] by A10,MCART_1:11; end; theorem Th33: for S, T being RelStr, X being Subset of [:S,T:] holds proj1 uparrow X c= uparrow proj1 X & proj2 uparrow X c= uparrow proj2 X proof let S, T be RelStr, X be Subset of [:S,T:]; A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; hereby let a be set; assume a in proj1 uparrow X; then consider b being set such that A2: [a,b] in uparrow X by FUNCT_5:def 1; A3: a in the carrier of S & b in the carrier of T by A1,A2,ZFMISC_1:106; then reconsider S' = S, T' = T as non empty RelStr by STRUCT_0:def 1; reconsider a' = a as Element of S' by A3; reconsider b' = b as Element of T' by A3; consider c being Element of [:S',T':] such that A4: [a',b'] >= c & c in X by A2,WAYBEL_0:def 16; A5: c = [c`1,c`2] by A1,MCART_1:23; then A6: a' >= c`1 by A4,YELLOW_3:11; c`1 in proj1 X by A4,A5,FUNCT_5:4; hence a in uparrow proj1 X by A6,WAYBEL_0:def 16; end; let b be set; assume b in proj2 uparrow X; then consider a being set such that A7: [a,b] in uparrow X by FUNCT_5:def 2; A8: a in the carrier of S & b in the carrier of T by A1,A7,ZFMISC_1:106; then reconsider S' = S, T' = T as non empty RelStr by STRUCT_0:def 1; reconsider a' = a as Element of S' by A8; reconsider b' = b as Element of T' by A8; consider c being Element of [:S',T':] such that A9: [a',b'] >= c & c in X by A7,WAYBEL_0:def 16; A10: c = [c`1,c`2] by A1,MCART_1:23; then A11: b' >= c`2 by A9,YELLOW_3:11; c`2 in proj2 X by A9,A10,FUNCT_5:4; hence b in uparrow proj2 X by A11,WAYBEL_0:def 16; end; theorem for S being RelStr, T being reflexive RelStr, X being Subset of [:S,T:] holds proj1 uparrow X = uparrow proj1 X proof let S be RelStr, T be reflexive RelStr, X be Subset of [:S,T:]; A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; thus proj1 uparrow X c= uparrow proj1 X by Th33; let a be set; assume A2: a in uparrow proj1 X; then reconsider S' = S as non empty RelStr by STRUCT_0:def 1; reconsider a' = a as Element of S' by A2; consider b being Element of S' such that A3: b <= a' & b in proj1 X by A2,WAYBEL_0:def 16; consider b2 being set such that A4: [b,b2] in X by A3,FUNCT_5:def 1; A5: b2 in the carrier of T by A1,A4,ZFMISC_1:106; then reconsider T' = T as non empty reflexive RelStr by STRUCT_0:def 1; reconsider b2 as Element of T' by A5; b2 <= b2; then [b,b2] <= [a',b2] by A3,YELLOW_3:11; then [a',b2] in uparrow X by A4,WAYBEL_0:def 16; hence a in proj1 uparrow X by FUNCT_5:def 1; end; theorem for S being reflexive RelStr, T being RelStr, X being Subset of [:S,T:] holds proj2 uparrow X = uparrow proj2 X proof let S be reflexive RelStr, T be RelStr, X be Subset of [:S,T:]; A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; thus proj2 uparrow X c= uparrow proj2 X by Th33; let c be set; assume A2: c in uparrow proj2 X; then reconsider T' = T as non empty RelStr by STRUCT_0:def 1; reconsider c' = c as Element of T' by A2; consider b being Element of T' such that A3: b <= c' & b in proj2 X by A2,WAYBEL_0:def 16; consider b1 being set such that A4: [b1,b] in X by A3,FUNCT_5:def 2; A5: b1 in the carrier of S by A1,A4,ZFMISC_1:106; then reconsider S' = S as non empty reflexive RelStr by STRUCT_0:def 1; reconsider b1 as Element of S' by A5; b1 <= b1; then [b1,b] <= [b1,c'] by A3,YELLOW_3:11; then [b1,c'] in uparrow X by A4,WAYBEL_0:def 16; hence c in proj2 uparrow X by FUNCT_5:def 2; end; theorem for S, T being non empty RelStr, s being Element of S, t being Element of T holds [:downarrow s,downarrow t:] = downarrow [s,t] proof let S, T be non empty RelStr, s be Element of S, t be Element of T; A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; hereby let x be set; assume x in [:downarrow s,downarrow t:]; then consider x1, x2 being set such that A2: x1 in downarrow s & x2 in downarrow t & x = [x1,x2] by ZFMISC_1:def 2; reconsider x1 as Element of S by A2; reconsider x2 as Element of T by A2; s >= x1 & t >= x2 by A2,WAYBEL_0:17; then [s,t] >= [x1,x2] by YELLOW_3:11; hence x in downarrow [s,t] by A2,WAYBEL_0:17; end; let x be set; assume A3: x in downarrow [s,t]; then reconsider x' = x as Element of [:S,T:]; A4: x' = [x'`1,x'`2] by A1,MCART_1:23; [s,t] >= x' by A3,WAYBEL_0:17; then s >= x'`1 & t >= x'`2 by A4,YELLOW_3:11; then x`1 in downarrow s & x`2 in downarrow t by WAYBEL_0:17; hence x in [:downarrow s,downarrow t:] by A4,MCART_1:11; end; theorem Th37: for S, T being non empty RelStr, x being Element of [:S,T:] holds proj1 downarrow x c= downarrow x`1 & proj2 downarrow x c= downarrow x`2 proof let S, T be non empty RelStr, x be Element of [:S,T:]; A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; then A2: x = [x`1,x`2] by MCART_1:23; hereby let a be set; assume a in proj1 downarrow x; then consider b being set such that A3: [a,b] in downarrow x by FUNCT_5:def 1; A4: a in the carrier of S & b in the carrier of T by A1,A3,ZFMISC_1:106; then reconsider a' = a as Element of S; reconsider b as Element of T by A4; [a',b] <= x by A3,WAYBEL_0:17; then a' <= x`1 by A2,YELLOW_3:11; hence a in downarrow x`1 by WAYBEL_0:17; end; let b be set; assume b in proj2 downarrow x; then consider a being set such that A5: [a,b] in downarrow x by FUNCT_5:def 2; A6: a in the carrier of S & b in the carrier of T by A1,A5,ZFMISC_1:106; then reconsider b' = b as Element of T; reconsider a as Element of S by A6; [a,b'] <= x by A5,WAYBEL_0:17; then b' <= x`2 by A2,YELLOW_3:11; hence b in downarrow x`2 by WAYBEL_0:17; end; theorem for S being non empty RelStr, T being non empty reflexive RelStr, x being Element of [:S,T:] holds proj1 downarrow x = downarrow x`1 proof let S be non empty RelStr, T be non empty reflexive RelStr, x be Element of [:S,T:]; the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; then A1: x = [x`1,x`2] by MCART_1:23; thus proj1 downarrow x c= downarrow x`1 by Th37; let a be set; assume A2: a in downarrow x`1; then reconsider a' = a as Element of S; A3: a' <= x`1 by A2,WAYBEL_0:17; x`2 <= x`2; then [a',x`2] <= [x`1,x`2] by A3,YELLOW_3:11; then [a',x`2] in downarrow [x`1,x`2] by WAYBEL_0:17; hence a in proj1 downarrow x by A1,FUNCT_5:def 1; end; theorem for S being non empty reflexive RelStr, T being non empty RelStr, x being Element of [:S,T:] holds proj2 downarrow x = downarrow x`2 proof let S be non empty reflexive RelStr, T be non empty RelStr, x be Element of [:S,T:]; the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; then A1: x = [x`1,x`2] by MCART_1:23; thus proj2 downarrow x c= downarrow x`2 by Th37; let b be set; assume A2: b in downarrow x`2; then reconsider b' = b as Element of T; A3: b' <= x`2 by A2,WAYBEL_0:17; x`1 <= x`1; then [x`1,b'] <= [x`1,x`2] by A3,YELLOW_3:11; then [x`1,b'] in downarrow [x`1,x`2] by WAYBEL_0:17; hence b in proj2 downarrow x by A1,FUNCT_5:def 2; end; theorem for S, T being non empty RelStr, s being Element of S, t being Element of T holds [:uparrow s,uparrow t:] = uparrow [s,t] proof let S, T be non empty RelStr, s be Element of S, t be Element of T; A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; hereby let x be set; assume x in [:uparrow s,uparrow t:]; then consider x1, x2 being set such that A2: x1 in uparrow s & x2 in uparrow t & x = [x1,x2] by ZFMISC_1:def 2; reconsider x1 as Element of S by A2; reconsider x2 as Element of T by A2; s <= x1 & t <= x2 by A2,WAYBEL_0:18; then [s,t] <= [x1,x2] by YELLOW_3:11; hence x in uparrow [s,t] by A2,WAYBEL_0:18; end; let x be set; assume A3: x in uparrow [s,t]; then reconsider x' = x as Element of [:S,T:]; A4: x' = [x'`1,x'`2] by A1,MCART_1:23; [s,t] <= x' by A3,WAYBEL_0:18; then s <= x'`1 & t <= x'`2 by A4,YELLOW_3:11; then x`1 in uparrow s & x`2 in uparrow t by WAYBEL_0:18; hence x in [:uparrow s,uparrow t:] by A4,MCART_1:11; end; theorem Th41: for S, T being non empty RelStr, x being Element of [:S,T:] holds proj1 uparrow x c= uparrow x`1 & proj2 uparrow x c= uparrow x`2 proof let S, T be non empty RelStr, x be Element of [:S,T:]; A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; then A2: x = [x`1,x`2] by MCART_1:23; hereby let a be set; assume a in proj1 uparrow x; then consider b being set such that A3: [a,b] in uparrow x by FUNCT_5:def 1; A4: a in the carrier of S & b in the carrier of T by A1,A3,ZFMISC_1:106; then reconsider a' = a as Element of S; reconsider b as Element of T by A4; [a',b] >= x by A3,WAYBEL_0:18; then a' >= x`1 by A2,YELLOW_3:11; hence a in uparrow x`1 by WAYBEL_0:18; end; let b be set; assume b in proj2 uparrow x; then consider a being set such that A5: [a,b] in uparrow x by FUNCT_5:def 2; A6: a in the carrier of S & b in the carrier of T by A1,A5,ZFMISC_1:106; then reconsider b' = b as Element of T; reconsider a as Element of S by A6; [a,b'] >= x by A5,WAYBEL_0:18; then b' >= x`2 by A2,YELLOW_3:11; hence b in uparrow x`2 by WAYBEL_0:18; end; theorem for S being non empty RelStr, T being non empty reflexive RelStr, x being Element of [:S,T:] holds proj1 uparrow x = uparrow x`1 proof let S be non empty RelStr, T be non empty reflexive RelStr, x be Element of [:S,T:]; the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; then A1: x = [x`1,x`2] by MCART_1:23; thus proj1 uparrow x c= uparrow x`1 by Th41; let a be set; assume A2: a in uparrow x`1; then reconsider a' = a as Element of S; A3: a' >= x`1 by A2,WAYBEL_0:18; x`2 <= x`2; then [a',x`2] >= [x`1,x`2] by A3,YELLOW_3:11; then [a',x`2] in uparrow [x`1,x`2] by WAYBEL_0:18; hence a in proj1 uparrow x by A1,FUNCT_5:def 1; end; theorem for S being non empty reflexive RelStr, T being non empty RelStr, x being Element of [:S,T:] holds proj2 uparrow x = uparrow x`2 proof let S be non empty reflexive RelStr, T be non empty RelStr, x be Element of [:S,T:]; the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; then A1: x = [x`1,x`2] by MCART_1:23; thus proj2 uparrow x c= uparrow x`2 by Th41; let b be set; assume A2: b in uparrow x`2; then reconsider b' = b as Element of T; A3: b' >= x`2 by A2,WAYBEL_0:18; x`1 <= x`1; then [x`1,b'] >= [x`1,x`2] by A3,YELLOW_3:11; then [x`1,b'] in uparrow [x`1,x`2] by WAYBEL_0:18; hence b in proj2 uparrow x by A1,FUNCT_5:def 2; end; theorem Th44: for S, T being up-complete (non empty Poset), s being Element of S, t being Element of T holds [:waybelow s,waybelow t:] = waybelow [s,t] proof let S, T be up-complete (non empty Poset), s be Element of S, t be Element of T; A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; hereby let x be set; assume x in [:waybelow s,waybelow t:]; then consider x1, x2 being set such that A2: x1 in waybelow s & x2 in waybelow t & x = [x1,x2] by ZFMISC_1:def 2; reconsider x1 as Element of S by A2; reconsider x2 as Element of T by A2; s >> x1 & t >> x2 by A2,WAYBEL_3:7; then [s,t] >> [x1,x2] by Th19; hence x in waybelow [s,t] by A2,WAYBEL_3:7; end; let x be set; assume A3: x in waybelow [s,t]; then reconsider x' = x as Element of [:S,T:]; A4: x' = [x'`1,x'`2] by A1,MCART_1:23; [s,t] >> x' by A3,WAYBEL_3:7; then s >> x'`1 & t >> x'`2 by A4,Th19; then x`1 in waybelow s & x`2 in waybelow t by WAYBEL_3:7; hence x in [:waybelow s,waybelow t:] by A4,MCART_1:11; end; theorem Th45: for S, T being antisymmetric up-complete (non empty reflexive RelStr), x being Element of [:S,T:] holds proj1 waybelow x c= waybelow x`1 & proj2 waybelow x c= waybelow x`2 proof let S, T be antisymmetric up-complete (non empty reflexive RelStr), x be Element of [:S,T:]; A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; then A2: x = [x`1,x`2] by MCART_1:23; hereby let a be set; assume a in proj1 waybelow x; then consider b being set such that A3: [a,b] in waybelow x by FUNCT_5:def 1; A4: a in the carrier of S & b in the carrier of T by A1,A3,ZFMISC_1:106; then reconsider a' = a as Element of S; reconsider b as Element of T by A4; [a',b] << x by A3,WAYBEL_3:7; then a' << x`1 by A2,Th18; hence a in waybelow x`1 by WAYBEL_3:7; end; let b be set; assume b in proj2 waybelow x; then consider a being set such that A5: [a,b] in waybelow x by FUNCT_5:def 2; A6: a in the carrier of S & b in the carrier of T by A1,A5,ZFMISC_1:106; then reconsider b' = b as Element of T; reconsider a as Element of S by A6; [a,b'] << x by A5,WAYBEL_3:7; then b' << x`2 by A2,Th18; hence b in waybelow x`2 by WAYBEL_3:7; end; theorem Th46: for S being up-complete (non empty Poset), T being up-complete lower-bounded (non empty Poset), x being Element of [:S,T:] holds proj1 waybelow x = waybelow x`1 proof let S be up-complete (non empty Poset), T be up-complete lower-bounded (non empty Poset), x be Element of [:S,T:]; the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; then A1: x = [x`1,x`2] by MCART_1:23; thus proj1 waybelow x c= waybelow x`1 by Th45; let a be set; assume A2: a in waybelow x`1; then reconsider a' = a as Element of S; A3: a' << x`1 by A2,WAYBEL_3:7; Bottom T << x`2 by WAYBEL_3:4; then [a',Bottom T] << [x`1,x`2] by A3,Th19; then [a',Bottom T] in waybelow [x`1,x`2] by WAYBEL_3:7; hence a in proj1 waybelow x by A1,FUNCT_5:def 1; end; theorem Th47: for S being up-complete lower-bounded (non empty Poset), T being up-complete (non empty Poset), x being Element of [:S,T:] holds proj2 waybelow x = waybelow x`2 proof let S be up-complete lower-bounded (non empty Poset), T be up-complete (non empty Poset), x be Element of [:S,T:]; the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; then A1: x = [x`1,x`2] by MCART_1:23; thus proj2 waybelow x c= waybelow x`2 by Th45; let a be set; assume A2: a in waybelow x`2; then reconsider a' = a as Element of T; A3: a' << x`2 by A2,WAYBEL_3:7; Bottom S << x`1 by WAYBEL_3:4; then [Bottom S,a'] << [x`1,x`2] by A3,Th19; then [Bottom S,a'] in waybelow [x`1,x`2] by WAYBEL_3:7; hence a in proj2 waybelow x by A1,FUNCT_5:def 2; end; theorem for S, T being up-complete (non empty Poset), s being Element of S, t being Element of T holds [:wayabove s,wayabove t:] = wayabove [s,t] proof let S, T be up-complete (non empty Poset), s be Element of S, t be Element of T; A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; hereby let x be set; assume x in [:wayabove s,wayabove t:]; then consider x1, x2 being set such that A2: x1 in wayabove s & x2 in wayabove t & x = [x1,x2] by ZFMISC_1:def 2; reconsider x1 as Element of S by A2; reconsider x2 as Element of T by A2; s << x1 & t << x2 by A2,WAYBEL_3:8; then [s,t] << [x1,x2] by Th19; hence x in wayabove [s,t] by A2,WAYBEL_3:8; end; let x be set; assume A3: x in wayabove [s,t]; then reconsider x' = x as Element of [:S,T:]; A4: x' = [x'`1,x'`2] by A1,MCART_1:23; [s,t] << x' by A3,WAYBEL_3:8; then s << x'`1 & t << x'`2 by A4,Th19; then x`1 in wayabove s & x`2 in wayabove t by WAYBEL_3:8; hence x in [:wayabove s,wayabove t:] by A4,MCART_1:11; end; theorem for S, T being antisymmetric up-complete (non empty reflexive RelStr), x being Element of [:S,T:] holds proj1 wayabove x c= wayabove x`1 & proj2 wayabove x c= wayabove x`2 proof let S, T be antisymmetric up-complete (non empty reflexive RelStr), x be Element of [:S,T:]; A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; then A2: x = [x`1,x`2] by MCART_1:23; hereby let a be set; assume a in proj1 wayabove x; then consider b being set such that A3: [a,b] in wayabove x by FUNCT_5:def 1; A4: a in the carrier of S & b in the carrier of T by A1,A3,ZFMISC_1:106; then reconsider a' = a as Element of S; reconsider b as Element of T by A4; [a',b] >> x by A3,WAYBEL_3:8; then a' >> x`1 by A2,Th18; hence a in wayabove x`1 by WAYBEL_3:8; end; let b be set; assume b in proj2 wayabove x; then consider a being set such that A5: [a,b] in wayabove x by FUNCT_5:def 2; A6: a in the carrier of S & b in the carrier of T by A1,A5,ZFMISC_1:106; then reconsider b' = b as Element of T; reconsider a as Element of S by A6; [a,b'] >> x by A5,WAYBEL_3:8; then b' >> x`2 by A2,Th18; hence b in wayabove x`2 by WAYBEL_3:8; end; theorem Th50: for S, T being up-complete (non empty Poset), s being Element of S, t being Element of T holds [:compactbelow s,compactbelow t:] = compactbelow [s,t] proof let S, T be up-complete (non empty Poset), s be Element of S, t be Element of T; A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; hereby let x be set; assume x in [:compactbelow s,compactbelow t:]; then consider x1, x2 being set such that A2: x1 in compactbelow s & x2 in compactbelow t & x = [x1,x2] by ZFMISC_1:def 2; reconsider x1 as Element of S by A2; reconsider x2 as Element of T by A2; s >= x1 & t >= x2 by A2,WAYBEL_8:4; then A3: [s,t] >= [x1,x2] by YELLOW_3:11; A4: [x1,x2]`1 = x1 & [x1,x2]`2 = x2 by MCART_1:7; x1 is compact & x2 is compact by A2,WAYBEL_8:4; then [x1,x2] is compact by A4,Th23; hence x in compactbelow [s,t] by A2,A3,WAYBEL_8:4; end; let x be set; assume A5: x in compactbelow [s,t]; then reconsider x' = x as Element of [:S,T:]; A6: x' = [x'`1,x'`2] by A1,MCART_1:23; A7: [s,t] >= x' & x' is compact by A5,WAYBEL_8:4; then A8: s >= x'`1 & t >= x'`2 by A6,YELLOW_3:11; x'`1 is compact & x'`2 is compact by A7,Th22; then x`1 in compactbelow s & x`2 in compactbelow t by A8,WAYBEL_8:4; hence x in [:compactbelow s,compactbelow t:] by A6,MCART_1:11; end; theorem Th51: for S, T being antisymmetric up-complete (non empty reflexive RelStr), x being Element of [:S,T:] holds proj1 compactbelow x c= compactbelow x`1 & proj2 compactbelow x c= compactbelow x`2 proof let S, T be antisymmetric up-complete (non empty reflexive RelStr), x be Element of [:S,T:]; A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; then A2: x = [x`1,x`2] by MCART_1:23; hereby let a be set; assume a in proj1 compactbelow x; then consider b being set such that A3: [a,b] in compactbelow x by FUNCT_5:def 1; A4: a in the carrier of S & b in the carrier of T by A1,A3,ZFMISC_1:106; then reconsider a' = a as Element of S; reconsider b as Element of T by A4; A5: [a',b]`1 = a' & [a',b]`2 = b by MCART_1:7; [a',b] <= x & [a',b] is compact by A3,WAYBEL_8:4; then a' <= x`1 & a' is compact by A2,A5,Th22,YELLOW_3:11; hence a in compactbelow x`1 by WAYBEL_8:4; end; let b be set; assume b in proj2 compactbelow x; then consider a being set such that A6: [a,b] in compactbelow x by FUNCT_5:def 2; A7: a in the carrier of S & b in the carrier of T by A1,A6,ZFMISC_1:106; then reconsider b' = b as Element of T; reconsider a as Element of S by A7; A8: [a,b']`1 = a & [a,b']`2 = b' by MCART_1:7; [a,b'] <= x & [a,b'] is compact by A6,WAYBEL_8:4; then b' <= x`2 & b' is compact by A2,A8,Th22,YELLOW_3:11; hence b in compactbelow x`2 by WAYBEL_8:4; end; theorem Th52: for S being up-complete (non empty Poset), T being up-complete lower-bounded (non empty Poset), x being Element of [:S,T:] holds proj1 compactbelow x = compactbelow x`1 proof let S be up-complete (non empty Poset), T be up-complete lower-bounded (non empty Poset), x be Element of [:S,T:]; the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; then A1: x = [x`1,x`2] by MCART_1:23; thus proj1 compactbelow x c= compactbelow x`1 by Th51; let a be set; assume A2: a in compactbelow x`1; then reconsider a' = a as Element of S; A3: a' <= x`1 & a' is compact by A2,WAYBEL_8:4; Bottom T <= x`2 by YELLOW_0:44; then A4: [a',Bottom T] <= [x`1,x`2] by A3,YELLOW_3:11; A5: [a',Bottom T]`1 = a' & [a',Bottom T]`2 = Bottom T by MCART_1:7; Bottom T is compact by WAYBEL_3:15; then [a',Bottom T] is compact by A3,A5,Th23; then [a',Bottom T] in compactbelow [x`1,x`2] by A4,WAYBEL_8:4; hence a in proj1 compactbelow x by A1,FUNCT_5:def 1; end; theorem Th53: for S being up-complete lower-bounded (non empty Poset), T being up-complete (non empty Poset), x being Element of [:S,T:] holds proj2 compactbelow x = compactbelow x`2 proof let S be up-complete lower-bounded (non empty Poset), T be up-complete (non empty Poset), x be Element of [:S,T:]; the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; then A1: x = [x`1,x`2] by MCART_1:23; thus proj2 compactbelow x c= compactbelow x`2 by Th51; let a be set; assume A2: a in compactbelow x`2; then reconsider a' = a as Element of T; A3: a' <= x`2 & a' is compact by A2,WAYBEL_8:4; Bottom S <= x`1 by YELLOW_0:44; then A4: [Bottom S,a'] <= [x`1,x`2] by A3,YELLOW_3:11; A5: [Bottom S,a']`1 = Bottom S & [Bottom S,a']`2 = a' by MCART_1:7; Bottom S is compact by WAYBEL_3:15; then [Bottom S,a'] is compact by A3,A5,Th23; then [Bottom S,a'] in compactbelow [x`1,x`2] by A4,WAYBEL_8:4; hence a in proj2 compactbelow x by A1,FUNCT_5:def 2; end; definition let S be non empty reflexive RelStr; cluster empty -> Open Subset of S; coherence proof let X be Subset of S such that A1: X is empty; let x be Element of S; assume x in X; hence thesis by A1; end; end; theorem for S, T being antisymmetric up-complete (non empty reflexive RelStr), X being Subset of [:S,T:] st X is Open holds proj1 X is Open & proj2 X is Open proof let S, T be antisymmetric up-complete (non empty reflexive RelStr), X be Subset of [:S,T:] such that A1: for x being Element of [:S,T:] st x in X ex y being Element of [:S,T:] st y in X & y << x; A2: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; hereby let s be Element of S; assume s in proj1 X; then consider t being set such that A3: [s,t] in X by FUNCT_5:def 1; t in the carrier of T by A2,A3,ZFMISC_1:106; then reconsider t as Element of T; consider y being Element of [:S,T:] such that A4: y in X & y << [s,t] by A1,A3; take z = y`1; A5: y = [y`1,y`2] by A2,MCART_1:23; hence z in proj1 X by A4,FUNCT_5:def 1; thus z << s by A4,A5,Th18; end; let t be Element of T; assume t in proj2 X; then consider s being set such that A6: [s,t] in X by FUNCT_5:def 2; s in the carrier of S by A2,A6,ZFMISC_1:106; then reconsider s as Element of S; consider y being Element of [:S,T:] such that A7: y in X & y << [s,t] by A1,A6; take z = y`2; A8: y = [y`1,y`2] by A2,MCART_1:23; hence z in proj2 X by A7,FUNCT_5:def 2; thus z << t by A7,A8,Th18; end; theorem for S, T being up-complete (non empty Poset), X being Subset of S, Y being Subset of T st X is Open & Y is Open holds [:X,Y:] is Open proof let S, T be up-complete (non empty Poset), X be Subset of S, Y be Subset of T such that A1: for x being Element of S st x in X ex y being Element of S st y in X & y << x and A2: for x being Element of T st x in Y ex y being Element of T st y in Y & y << x; let x be Element of [:S,T:]; assume A3: x in [:X,Y:]; then A4: x = [x`1,x`2] by MCART_1:23; then x`1 in X by A3,ZFMISC_1:106; then consider s being Element of S such that A5: s in X & s << x`1 by A1; x`2 in Y by A3,A4,ZFMISC_1:106; then consider t being Element of T such that A6: t in Y & t << x`2 by A2; reconsider t as Element of T; take [s,t]; thus [s,t] in [:X,Y:] by A5,A6,ZFMISC_1:106; thus [s,t] << x by A4,A5,A6,Th19; end; theorem for S, T being antisymmetric up-complete (non empty reflexive RelStr), X being Subset of [:S,T:] st X is inaccessible holds proj1 X is inaccessible & proj2 X is inaccessible proof let S, T be antisymmetric up-complete (non empty reflexive RelStr), X be Subset of [:S,T:] such that A1: for D being non empty directed Subset of [:S,T:] st sup D in X holds D meets X; A2: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; hereby let D be non empty directed Subset of S; assume sup D in proj1 X; then consider t being set such that A3: [sup D, t] in X by FUNCT_5:def 1; t in the carrier of T by A2,A3,ZFMISC_1:106; then A4: t is Element of T; then reconsider t' = {t} as non empty directed Subset of T by WAYBEL_0:5; ex_sup_of [:D,t':],[:S,T:] by WAYBEL_0:75; then sup [:D,t':] = [sup proj1 [:D,t':], sup proj2 [:D,t':]] by YELLOW_3: 46 .= [sup D, sup proj2 [:D,t':]] by FUNCT_5:11 .= [sup D,sup t'] by FUNCT_5:11 .= [sup D,t] by A4,YELLOW_0:39; then [:D,{t}:] meets X by A1,A3; then consider x being set such that A5: x in [:D,{t}:] & x in X by XBOOLE_0:3; thus D meets proj1 X proof now take a = x`1; x = [a,x`2] by A5,MCART_1:23; hence a in D & a in proj1 X by A5,FUNCT_5:4,ZFMISC_1:106; end; hence thesis by XBOOLE_0:3; end; end; let D be non empty directed Subset of T; assume sup D in proj2 X; then consider s being set such that A6: [s,sup D] in X by FUNCT_5:def 2; s in the carrier of S by A2,A6,ZFMISC_1:106; then A7: s is Element of S; then reconsider s' = {s} as non empty directed Subset of S by WAYBEL_0:5; ex_sup_of [:s',D:],[:S,T:] by WAYBEL_0:75; then sup [:s',D:] = [sup proj1 [:s',D:], sup proj2 [:s',D:]] by YELLOW_3:46 .= [sup s', sup proj2 [:s',D:]] by FUNCT_5:11 .= [sup s',sup D] by FUNCT_5:11 .= [s,sup D] by A7,YELLOW_0:39; then [:{s},D:] meets X by A1,A6; then consider x being set such that A8: x in [:{s},D:] & x in X by XBOOLE_0:3; now take a = x`2; x = [x`1,a] by A8,MCART_1:23; hence a in D & a in proj2 X by A8,FUNCT_5:4,ZFMISC_1:106; end; hence thesis by XBOOLE_0:3; end; theorem for S, T being antisymmetric up-complete (non empty reflexive RelStr), X being upper Subset of S, Y being upper Subset of T st X is inaccessible & Y is inaccessible holds [:X,Y:] is inaccessible proof let S, T be antisymmetric up-complete (non empty reflexive RelStr), X be upper Subset of S, Y be upper Subset of T such that A1: for D being non empty directed Subset of S st sup D in X holds D meets X and A2: for D being non empty directed Subset of T st sup D in Y holds D meets Y; let D be non empty directed Subset of [:S,T:] such that A3: sup D in [:X,Y:]; A4: proj1 D is non empty directed & proj2 D is non empty directed by YELLOW_3:21,22; ex_sup_of D,[:S,T:] by WAYBEL_0:75; then sup D = [sup proj1 D, sup proj2 D] by YELLOW_3:46; then sup proj1 D in X & sup proj2 D in Y by A3,ZFMISC_1:106; then A5: proj1 D meets X & proj2 D meets Y by A1,A2,A4; then consider s being set such that A6: s in proj1 D & s in X by XBOOLE_0:3; consider t being set such that A7: t in proj2 D & t in Y by A5,XBOOLE_0:3; reconsider s as Element of S by A6; reconsider t as Element of T by A7; consider s2 being set such that A8: [s,s2] in D by A6,FUNCT_5:def 1; A9: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; then s2 in the carrier of T by A8,ZFMISC_1:106; then reconsider s2 as Element of T; consider t1 being set such that A10: [t1,t] in D by A7,FUNCT_5:def 2; t1 in the carrier of S by A9,A10,ZFMISC_1:106; then reconsider t1 as Element of S; consider z being Element of [:S,T:] such that A11: z in D and A12: [s,s2] <= z & [t1,t] <= z by A8,A10,WAYBEL_0:def 1; now take z; thus z in D by A11; A13:z = [z`1,z`2] by A9,MCART_1:23; then s <= z`1 & t <= z`2 by A12,YELLOW_3:11; then z`1 in X & z`2 in Y by A6,A7,WAYBEL_0:def 20; hence z in [:X,Y:] by A13,ZFMISC_1:106; end; hence thesis by XBOOLE_0:3; end; theorem for S, T being antisymmetric up-complete (non empty reflexive RelStr), X being Subset of S, Y being Subset of T st [:X,Y:] is directly_closed holds (Y <> {} implies X is directly_closed) & (X <> {} implies Y is directly_closed) proof let S, T be antisymmetric up-complete (non empty reflexive RelStr), X be Subset of S, Y be Subset of T such that A1: for D being non empty directed Subset of [:S,T:] st D c= [:X,Y:] holds sup D in [:X,Y:]; hereby assume A2: Y <> {}; thus X is directly_closed proof let D be non empty directed Subset of S such that A3: D c= X; consider t being set such that A4: t in Y by A2,XBOOLE_0:def 1; A5: t is Element of T by A4; then reconsider t' = {t} as non empty directed Subset of T by WAYBEL_0: 5; t' c= Y by A4,ZFMISC_1:37; then A6: [:D,t':] c= [:X,Y:] by A3,ZFMISC_1:119; ex_sup_of [:D,t':],[:S,T:] by WAYBEL_0:75; then A7: sup [:D,t':] = [sup proj1 [:D,t':], sup proj2 [:D,t':]] by YELLOW_3:46 .= [sup D, sup proj2 [:D,t':]] by FUNCT_5:11 .= [sup D,sup t'] by FUNCT_5:11 .= [sup D,t] by A5,YELLOW_0:39; sup [:D,t':] in [:X,Y:] by A1,A6; hence sup D in X by A7,ZFMISC_1:106; end; end; assume A8: X <> {}; let D be non empty directed Subset of T such that A9: D c= Y; consider s being set such that A10: s in X by A8,XBOOLE_0:def 1; A11: s is Element of S by A10; then reconsider s' = {s} as non empty directed Subset of S by WAYBEL_0:5; s' c= X by A10,ZFMISC_1:37; then A12: [:s',D:] c= [:X,Y:] by A9,ZFMISC_1:119; ex_sup_of [:s',D:],[:S,T:] by WAYBEL_0:75; then A13: sup [:s',D:] = [sup proj1 [:s',D:], sup proj2 [:s',D:]] by YELLOW_3: 46 .= [sup s',sup proj2 [:s',D:]] by FUNCT_5:11 .= [sup s',sup D] by FUNCT_5:11 .= [s,sup D] by A11,YELLOW_0:39; sup [:s',D:] in [:X,Y:] by A1,A12; hence sup D in Y by A13,ZFMISC_1:106; end; theorem for S, T being antisymmetric up-complete (non empty reflexive RelStr), X being Subset of S, Y being Subset of T st X is directly_closed & Y is directly_closed holds [:X,Y:] is directly_closed proof let S, T be antisymmetric up-complete (non empty reflexive RelStr), X be Subset of S, Y be Subset of T such that A1: for D being non empty directed Subset of S st D c= X holds sup D in X and A2: for D being non empty directed Subset of T st D c= Y holds sup D in Y; let D be non empty directed Subset of [:S,T:]; assume D c= [:X,Y:]; then A3: proj1 D c= X & proj2 D c= Y by FUNCT_5:13; proj1 D is non empty directed & proj2 D is non empty directed by YELLOW_3:21,22; then A4: sup proj1 D in X & sup proj2 D in Y by A1,A2,A3; ex_sup_of D,[:S,T:] by WAYBEL_0:75; then sup D = [sup proj1 D,sup proj2 D] by YELLOW_3:46; hence sup D in [:X,Y:] by A4,ZFMISC_1:106; end; theorem for S, T being antisymmetric up-complete (non empty reflexive RelStr), X being Subset of [:S,T:] st X has_the_property_(S) holds proj1 X has_the_property_(S) & proj2 X has_the_property_(S) proof let S, T be antisymmetric up-complete (non empty reflexive RelStr), X be Subset of [:S,T:] such that A1: for D being non empty directed Subset of [:S,T:] st sup D in X ex y being Element of [:S,T:] st y in D & for x being Element of [:S,T:] st x in D & x >= y holds x in X; A2: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; hereby let D be non empty directed Subset of S; assume sup D in proj1 X; then consider t being set such that A3: [sup D, t] in X by FUNCT_5:def 1; t in the carrier of T by A2,A3,ZFMISC_1:106; then reconsider t as Element of T; reconsider t' = {t} as non empty directed Subset of T by WAYBEL_0:5; ex_sup_of [:D,t':],[:S,T:] by WAYBEL_0:75; then sup [:D,t':] = [sup proj1 [:D,t':], sup proj2 [:D,t':]] by YELLOW_3: 46 .= [sup D, sup proj2 [:D,t':]] by FUNCT_5:11 .= [sup D,sup t'] by FUNCT_5:11 .= [sup D,t] by YELLOW_0:39; then consider y being Element of [:S,T:] such that A4: y in [:D,t':] and A5: for x being Element of [:S,T:] st x in [:D,t':] & x >= y holds x in X by A1,A3; take z = y`1; A6: y = [y`1,y`2] by A2,MCART_1:23; hence z in D by A4,ZFMISC_1:106; let x be Element of S; assume x in D; then A7: [x,t] in [:D,t':] by ZFMISC_1:129; assume A8: x >= z; A9: y`2 = t by A4,A6,ZFMISC_1:129; y`2 <= y`2; then [x,t] >= y by A6,A8,A9,YELLOW_3:11; then [x,t] in X by A5,A7; hence x in proj1 X by FUNCT_5:4; end; let D be non empty directed Subset of T; assume sup D in proj2 X; then consider s being set such that A10: [s,sup D] in X by FUNCT_5:def 2; s in the carrier of S by A2,A10,ZFMISC_1:106; then reconsider s as Element of S; reconsider s' = {s} as non empty directed Subset of S by WAYBEL_0:5; ex_sup_of [:s',D:],[:S,T:] by WAYBEL_0:75; then sup [:s',D:] = [sup proj1 [:s',D:], sup proj2 [:s',D:]] by YELLOW_3:46 .= [sup s', sup proj2 [:s',D:]] by FUNCT_5:11 .= [sup s',sup D] by FUNCT_5:11 .= [s,sup D] by YELLOW_0:39; then consider y being Element of [:S,T:] such that A11: y in [:s',D:] and A12: for x being Element of [:S,T:] st x in [:s',D:] & x >= y holds x in X by A1,A10; take z = y`2; A13: y = [y`1,y`2] by A2,MCART_1:23; hence z in D by A11,ZFMISC_1:106; let x be Element of T; assume x in D; then A14: [s,x] in [:s',D:] by ZFMISC_1:128; assume A15: x >= z; A16: y`1 = s by A11,A13,ZFMISC_1:128; y`1 <= y`1; then [s,x] >= y by A13,A15,A16,YELLOW_3:11; then [s,x] in X by A12,A14; hence x in proj2 X by FUNCT_5:4; end; theorem for S, T being up-complete (non empty Poset), X being Subset of S, Y being Subset of T st X has_the_property_(S) & Y has_the_property_(S) holds [:X,Y:] has_the_property_(S) proof let S, T be up-complete (non empty Poset), X be Subset of S, Y be Subset of T such that A1: for D being non empty directed Subset of S st sup D in X ex y being Element of S st y in D & for x being Element of S st x in D & x >= y holds x in X and A2: for D being non empty directed Subset of T st sup D in Y ex y being Element of T st y in D & for x being Element of T st x in D & x >= y holds x in Y; let D be non empty directed Subset of [:S,T:] such that A3: sup D in [:X,Y:]; A4: proj1 D is non empty directed & proj2 D is non empty directed by YELLOW_3:21,22; ex_sup_of D,[:S,T:] by WAYBEL_0:75; then sup D = [sup proj1 D,sup proj2 D] by YELLOW_3:46; then A5: sup proj1 D in X & sup proj2 D in Y by A3,ZFMISC_1:106; then consider s being Element of S such that A6: s in proj1 D and A7: for x being Element of S st x in proj1 D & x >= s holds x in X by A1,A4; consider t being Element of T such that A8: t in proj2 D and A9: for x being Element of T st x in proj2 D & x >= t holds x in Y by A2,A4,A5; consider s2 being set such that A10: [s,s2] in D by A6,FUNCT_5:def 1; A11: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; then s2 in the carrier of T by A10,ZFMISC_1:106; then reconsider s2 as Element of T; consider t1 being set such that A12: [t1,t] in D by A8,FUNCT_5:def 2; t1 in the carrier of S by A11,A12,ZFMISC_1:106; then reconsider t1 as Element of S; consider z being Element of [:S,T:] such that A13: z in D and A14: [s,s2] <= z & [t1,t] <= z by A10,A12,WAYBEL_0:def 1; take z; thus z in D by A13; let x be Element of [:S,T:] such that A15: x in D; assume x >= z; then A16: x`1 >= z`1 & x`2 >= z`2 by YELLOW_3:12; A17:x = [x`1,x`2] by A11,MCART_1:23; then A18:x`1 in proj1 D & x`2 in proj2 D by A15,FUNCT_5:4; z = [z`1,z`2] by A11,MCART_1:23; then s <= z`1 & t <= z`2 by A14,YELLOW_3:11; then x`1 >= s & x`2 >= t by A16,ORDERS_1:26; then x`1 in X & x`2 in Y by A7,A9,A18; hence x in [:X,Y:] by A17,ZFMISC_1:106; end; begin :: On the products of relational structures theorem Th62: for S, T being non empty reflexive RelStr st the RelStr of S = the RelStr of T & S is /\-complete holds T is /\-complete proof let S, T be non empty reflexive RelStr such that A1: the RelStr of S = the RelStr of T and A2: for X being non empty Subset of S ex x being Element of S st x is_<=_than X & for y being Element of S st y is_<=_than X holds x >= y; let X be non empty Subset of T; X is Subset of S by A1; then consider x being Element of S such that A3: x is_<=_than X and A4: for y being Element of S st y is_<=_than X holds x >= y by A2; reconsider z = x as Element of T by A1; take z; thus z is_<=_than X by A1,A3,YELLOW_0:2; let y be Element of T; reconsider s = y as Element of S by A1; assume y is_<=_than X; then s is_<=_than X by A1,YELLOW_0:2; then x >= s by A4; hence z >= y by A1,YELLOW_0:1; end; definition let S be /\-complete (non empty reflexive RelStr); cluster the RelStr of S -> /\-complete; coherence by Th62; end; definition let S, T be /\-complete (non empty reflexive RelStr); cluster [:S,T:] -> /\-complete; coherence proof let X be non empty Subset of [:S,T:]; proj1 X is non empty by YELLOW_3:21; then consider s being Element of S such that A1: s is_<=_than proj1 X and A2: for y being Element of S st y is_<=_than proj1 X holds s >= y by WAYBEL_0:def 40; proj2 X is non empty by YELLOW_3:21; then consider t being Element of T such that A3: t is_<=_than proj2 X and A4: for y being Element of T st y is_<=_than proj2 X holds t >= y by WAYBEL_0:def 40; take [s,t]; thus [s,t] is_<=_than X by A1,A3,YELLOW_3:34; let y be Element of [:S,T:]; the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; then A5: y = [y`1,y`2] by MCART_1:23; assume y is_<=_than X; then y`1 is_<=_than proj1 X & y`2 is_<=_than proj2 X by A5,YELLOW_3:34; then s >= y`1 & t >= y`2 by A2,A4; hence [s,t] >= y by A5,YELLOW_3:11; end; end; theorem for S, T being non empty reflexive RelStr st [:S,T:] is /\-complete holds S is /\-complete & T is /\-complete proof let S, T be non empty reflexive RelStr such that A1: for X being non empty Subset of [:S,T:] ex x being Element of [:S,T:] st x is_<=_than X & for y being Element of [:S,T:] st y is_<=_than X holds x >= y; A2: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; thus S is /\-complete proof let X be non empty Subset of S; consider t being Element of T; consider x being Element of [:S,T:] such that A3: x is_<=_than [:X,{t}:] and A4: for y being Element of [:S,T:] st y is_<=_than [:X,{t}:] holds x >= y by A1; take x`1; A5: x = [x`1,x`2] by A2,MCART_1:23; hence x`1 is_<=_than X by A3,YELLOW_3:32; let y be Element of S such that A6: y is_<=_than X; t <= t; then t is_<=_than {t} by YELLOW_0:7; then [y,t] is_<=_than [:X,{t}:] by A6,YELLOW_3:33; then x >= [y,t] by A4; hence x`1 >= y by A5,YELLOW_3:11; end; let X be non empty Subset of T; consider s being Element of S; consider x being Element of [:S,T:] such that A7: x is_<=_than [:{s},X:] and A8: for y being Element of [:S,T:] st y is_<=_than [:{s},X:] holds x >= y by A1; take x`2; A9: x = [x`1,x`2] by A2,MCART_1:23; hence x`2 is_<=_than X by A7,YELLOW_3:32; let y be Element of T such that A10: y is_<=_than X; s <= s; then s is_<=_than {s} by YELLOW_0:7; then [s,y] is_<=_than [:{s},X:] by A10,YELLOW_3:33; then x >= [s,y] by A8; hence x`2 >= y by A9,YELLOW_3:11; end; definition let S, T be complemented bounded with_infima with_suprema antisymmetric (non empty RelStr); cluster [:S,T:] -> complemented; coherence proof let x be Element of [:S,T:]; consider s being Element of S such that A1: s is_a_complement_of x`1 by WAYBEL_1:def 24; consider t being Element of T such that A2: t is_a_complement_of x`2 by WAYBEL_1:def 24; take [s,t]; the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; then [s,t]`1 = s & [s,t]`2 = t & x = [x`1,x`2] by MCART_1:7,23; hence [s,t] is_a_complement_of x by A1,A2,Th17; end; end; theorem for S, T being bounded with_infima with_suprema antisymmetric RelStr st [:S,T:] is complemented holds S is complemented & T is complemented proof let S, T be bounded with_infima with_suprema antisymmetric RelStr; assume A1: for x being Element of [:S,T:] ex y being Element of [:S,T:] st y is_a_complement_of x; A2: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; thus S is complemented proof let s be Element of S; consider t being Element of T; consider y being Element of [:S,T:] such that A3: y is_a_complement_of [s,t] by A1; take y`1; [s,t]`1 = s & [s,t]`2 = t & y = [y`1,y`2] by A2,MCART_1:7,23; hence y`1 is_a_complement_of s by A3,Th17; end; let t be Element of T; consider s being Element of S; consider y being Element of [:S,T:] such that A4: y is_a_complement_of [s,t] by A1; take y`2; [s,t]`1 = s & [s,t]`2 = t & y = [y`1,y`2] by A2,MCART_1:7,23; hence y`2 is_a_complement_of t by A4,Th17; end; definition let S, T be distributive with_infima with_suprema antisymmetric (non empty RelStr); cluster [:S,T:] -> distributive; coherence proof let x, y, z be Element of [:S,T:]; A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; A2: (x "/\" (y "\/" z))`1 = x`1 "/\" (y "\/" z)`1 by Th13 .= x`1 "/\" (y`1 "\/" z`1) by Th14 .= (x`1 "/\" y`1) "\/" (x`1 "/\" z`1) by WAYBEL_1:def 3 .= (x "/\" y)`1 "\/" (x`1 "/\" z`1) by Th13 .= (x "/\" y)`1 "\/" (x "/\" z)`1 by Th13 .= ((x "/\" y) "\/" (x "/\" z))`1 by Th14; (x "/\" (y "\/" z))`2 = x`2 "/\" (y "\/" z)`2 by Th13 .= x`2 "/\" (y`2 "\/" z`2) by Th14 .= (x`2 "/\" y`2) "\/" (x`2 "/\" z`2) by WAYBEL_1:def 3 .= (x "/\" y)`2 "\/" (x`2 "/\" z`2) by Th13 .= (x "/\" y)`2 "\/" (x "/\" z)`2 by Th13 .= ((x "/\" y) "\/" (x "/\" z))`2 by Th14; hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A1,A2,DOMAIN_1:12; end; end; theorem for S being with_infima with_suprema antisymmetric RelStr, T being with_infima with_suprema reflexive antisymmetric RelStr st [:S,T:] is distributive holds S is distributive proof let S be with_infima with_suprema antisymmetric RelStr, T be with_infima with_suprema reflexive antisymmetric RelStr such that A1: for x, y, z being Element of [:S,T:] holds x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z); let x, y, z be Element of S; consider t being Element of T; t <= t; then A2: t "\/" t = t & t "/\" t = t by YELLOW_0:24,25; thus x "/\" (y "\/" z) = [x "/\" (y "\/" z),t]`1 by MCART_1:7 .= ([x,t] "/\" [y "\/" z,t])`1 by A2,Th15 .= ([x,t] "/\" ([y,t] "\/" [z,t]))`1 by A2,Th16 .= (([x,t] "/\" [y,t]) "\/" ([x,t] "/\" [z,t]))`1 by A1 .= (([x "/\" y,t]) "\/" ([x,t] "/\" [z,t]))`1 by A2,Th15 .= ([x "/\" y,t] "\/" [x "/\" z,t])`1 by A2,Th15 .= [(x "/\" y) "\/" (x "/\" z),t]`1 by A2,Th16 .= (x "/\" y) "\/" (x "/\" z) by MCART_1:7; end; theorem for S being with_infima with_suprema reflexive antisymmetric RelStr, T being with_infima with_suprema antisymmetric RelStr st [:S,T:] is distributive holds T is distributive proof let S be with_infima with_suprema reflexive antisymmetric RelStr, T be with_infima with_suprema antisymmetric RelStr such that A1: for x, y, z being Element of [:S,T:] holds x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z); let x, y, z be Element of T; consider s being Element of S; s <= s; then A2: s "\/" s = s & s "/\" s = s by YELLOW_0:24,25; thus x "/\" (y "\/" z) = [s,x "/\" (y "\/" z)]`2 by MCART_1:7 .= ([s,x] "/\" [s,y "\/" z])`2 by A2,Th15 .= ([s,x] "/\" ([s,y] "\/" [s,z]))`2 by A2,Th16 .= (([s,x] "/\" [s,y]) "\/" ([s,x] "/\" [s,z]))`2 by A1 .= (([s,x "/\" y]) "\/" ([s,x] "/\" [s,z]))`2 by A2,Th15 .= ([s,x "/\" y] "\/" [s,x "/\" z])`2 by A2,Th15 .= [s,(x "/\" y) "\/" (x "/\" z)]`2 by A2,Th16 .= (x "/\" y) "\/" (x "/\" z) by MCART_1:7; end; definition let S, T be meet-continuous Semilattice; cluster [:S,T:] -> satisfying_MC; coherence proof let x be Element of [:S,T:], D be non empty directed Subset of [:S,T:]; A1: proj1 D is non empty directed by YELLOW_3:21,22; A2: proj2 D is non empty directed by YELLOW_3:21,22; A3: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; then A4: x = [x`1,x`2] by MCART_1:23; reconsider x' = {x} as non empty directed Subset of [:S,T:] by WAYBEL_0:5; ex_sup_of x' "/\" D,[:S,T:] & ex_sup_of D,[:S,T:] by WAYBEL_0:75; then A5: sup D = [sup proj1 D,sup proj2 D] by YELLOW_3:46; ex_sup_of x'"/\" D,[:S,T:] by WAYBEL_0:75; then A6: sup ({x} "/\" D) = [sup proj1 ({x} "/\" D), sup proj2 ({x} "/\" D)] by YELLOW_3:46; A7: (x "/\" sup D)`1 = x`1 "/\" (sup D)`1 by Th13 .= x`1 "/\" sup proj1 D by A5,MCART_1:7 .= sup ({x`1} "/\" proj1 D) by A1,WAYBEL_2:def 6 .= sup (proj1 {x} "/\" proj1 D) by A4,FUNCT_5:15 .= sup (proj1 ({x} "/\" D)) by Th24 .= (sup ({x} "/\" D))`1 by A6,MCART_1:7; (x "/\" sup D)`2 = x`2 "/\" (sup D)`2 by Th13 .= x`2 "/\" sup proj2 D by A5,MCART_1:7 .= sup ({x`2} "/\" proj2 D) by A2,WAYBEL_2:def 6 .= sup (proj2 {x} "/\" proj2 D) by A4,FUNCT_5:15 .= sup (proj2 ({x} "/\" D)) by Th24 .= (sup ({x} "/\" D))`2 by A6,MCART_1:7; hence x "/\" sup D = sup ({x} "/\" D) by A3,A7,DOMAIN_1:12; end; end; theorem for S, T being Semilattice st [:S,T:] is meet-continuous holds S is meet-continuous & T is meet-continuous proof let S, T be Semilattice such that A1: [:S,T:] is up-complete and A2: for x being Element of [:S,T:], D being non empty directed Subset of [:S,T:] holds x "/\" sup D = sup ({x} "/\" D); hereby thus S is up-complete by A1,WAYBEL_2:11; let s be Element of S, D be non empty directed Subset of S; consider t being Element of T; reconsider t' = {t} as non empty directed Subset of T by WAYBEL_0:5; ex_sup_of [:D,t':],[:S,T:] by A1,WAYBEL_0:75; then A3: sup [:D,t':] = [sup proj1 [:D,t':], sup proj2 [:D,t':]] by YELLOW_3: 46; reconsider ST = {[s,t]} as non empty directed Subset of [:S,T:] by WAYBEL_0:5; ex_sup_of ST "/\" [:D,t':],[:S,T:] by A1,WAYBEL_0:75; then A4: sup ({[s,t]} "/\" [:D,t':]) = [sup proj1 ({[s,t]} "/\" [:D,t':]), sup proj2 ({[s,t]} "/\" [:D,t':])] by YELLOW_3:46; thus sup ({s} "/\" D) = sup (proj1 {[s,t]} "/\" D) by FUNCT_5:15 .= sup (proj1 {[s,t]} "/\" proj1 [:D,t':]) by FUNCT_5:11 .= sup proj1 ({[s,t]} "/\" [:D,t':]) by Th24 .= (sup ({[s,t]} "/\" [:D,t':]))`1 by A4,MCART_1:7 .= ([s,t] "/\" sup [:D,t':] )`1 by A2 .= [s,t]`1 "/\" (sup [:D,t':])`1 by Th13 .= s "/\" (sup [:D,t':])`1 by MCART_1:7 .= s "/\" sup proj1 [:D,t':] by A3,MCART_1:7 .= s "/\" sup D by FUNCT_5:11; end; thus T is up-complete by A1,WAYBEL_2:11; let t be Element of T, D be non empty directed Subset of T; consider s being Element of S; reconsider s' = {s} as non empty directed Subset of S by WAYBEL_0:5; ex_sup_of [:s',D:],[:S,T:] by A1,WAYBEL_0:75; then A5: sup [:s',D:] = [sup proj1 [:s',D:], sup proj2 [:s',D:]] by YELLOW_3:46 ; reconsider ST = {[s,t]} as non empty directed Subset of [:S,T:] by WAYBEL_0:5; ex_sup_of ST "/\" [:s',D:],[:S,T:] by A1,WAYBEL_0:75; then A6: sup ({[s,t]} "/\" [:s',D:]) = [sup proj1 ({[s,t]} "/\" [:s',D:]), sup proj2 ({[s,t]} "/\" [:s',D:])] by YELLOW_3:46; thus sup ({t} "/\" D) = sup (proj2 {[s,t]} "/\" D) by FUNCT_5:15 .= sup (proj2 {[s,t]} "/\" proj2 [:s',D:]) by FUNCT_5:11 .= sup proj2 ({[s,t]} "/\" [:s',D:]) by Th24 .= (sup ({[s,t]} "/\" [:s',D:]))`2 by A6,MCART_1:7 .= ([s,t] "/\" sup [:s',D:] )`2 by A2 .= [s,t]`2 "/\" (sup [:s',D:])`2 by Th13 .= t "/\" (sup [:s',D:])`2 by MCART_1:7 .= t "/\" sup proj2 [:s',D:] by A5,MCART_1:7 .= t "/\" sup D by FUNCT_5:11; end; definition let S, T be satisfying_axiom_of_approximation up-complete /\-complete (non empty Poset); cluster [:S,T:] -> satisfying_axiom_of_approximation; coherence proof let x be Element of [:S,T:]; A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; ex_sup_of waybelow x,[:S,T:] by WAYBEL_0:75; then A2: sup waybelow x = [sup proj1 waybelow x,sup proj2 waybelow x] by YELLOW_3:46; then A3: (sup waybelow x)`1 = sup proj1 waybelow x by MCART_1:7 .= sup waybelow x`1 by Th46 .= x`1 by WAYBEL_3:def 5; (sup waybelow x)`2 = sup proj2 waybelow x by A2,MCART_1:7 .= sup waybelow x`2 by Th47 .= x`2 by WAYBEL_3:def 5; hence x = sup waybelow x by A1,A3,DOMAIN_1:12; end; end; definition let S, T be continuous /\-complete (non empty Poset); cluster [:S,T:] -> continuous; coherence proof thus for x being Element of [:S,T:] holds waybelow x is non empty directed; thus [:S,T:] is up-complete satisfying_axiom_of_approximation; end; end; theorem for S, T being up-complete lower-bounded (non empty Poset) st [:S,T:] is continuous holds S is continuous & T is continuous proof let S, T be up-complete lower-bounded (non empty Poset) such that A1: for x being Element of [:S,T:] holds waybelow x is non empty directed and A2: [:S,T:] is up-complete satisfying_axiom_of_approximation; A3: now let x be Element of [:S,T:]; waybelow x is non empty directed by A1; hence ex_sup_of waybelow x,[:S,T:] by WAYBEL_0:75; end; hereby hereby let s be Element of S; consider t being Element of T; A4: [:waybelow s,waybelow t:] = waybelow [s,t] by Th44; A5: proj1 [:waybelow s,waybelow t:] = waybelow s by FUNCT_5:11; waybelow [s,t] is directed by A1; hence waybelow s is non empty directed by A4,A5,YELLOW_3:22; end; thus S is up-complete; thus S is satisfying_axiom_of_approximation proof let s be Element of S; consider t being Element of T; waybelow [s,t] is directed by A1; then ex_sup_of waybelow [s,t], [:S,T:] by WAYBEL_0:75; then A6: sup waybelow [s,t] = [sup proj1 waybelow [s,t],sup proj2 waybelow [s,t]] by Th5; thus s = [s,t]`1 by MCART_1:7 .= (sup waybelow [s,t])`1 by A2,WAYBEL_3:def 5 .= sup proj1 waybelow [s,t] by A6,MCART_1:7 .= sup waybelow [s,t]`1 by Th46 .= sup waybelow s by MCART_1:7; end; end; hereby let t be Element of T; consider s being Element of S; A7: [:waybelow s,waybelow t:] = waybelow [s,t] by Th44; A8: proj2 [:waybelow s,waybelow t:] = waybelow t by FUNCT_5:11; waybelow [s,t] is directed by A1; hence waybelow t is non empty directed by A7,A8,YELLOW_3:22; end; thus T is up-complete; let t be Element of T; consider s being Element of S; ex_sup_of waybelow [s,t], [:S,T:] by A3; then A9: sup waybelow [s,t] = [sup proj1 waybelow [s,t],sup proj2 waybelow [s,t ]] by Th5; thus t = [s,t]`2 by MCART_1:7 .= (sup waybelow [s,t])`2 by A2,WAYBEL_3:def 5 .= sup proj2 waybelow [s,t] by A9,MCART_1:7 .= sup waybelow [s,t]`2 by Th47 .= sup waybelow t by MCART_1:7; end; definition let S, T be satisfying_axiom_K up-complete lower-bounded sup-Semilattice; cluster [:S,T:] -> satisfying_axiom_K; coherence proof let x be Element of [:S,T:]; A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2; A2: sup compactbelow x = [sup proj1 compactbelow x,sup proj2 compactbelow x] by YELLOW_3:46; then A3: (sup compactbelow x)`1 = sup proj1 compactbelow x by MCART_1:7 .= sup compactbelow x`1 by Th52 .= x`1 by WAYBEL_8:def 3; (sup compactbelow x)`2 = sup proj2 compactbelow x by A2,MCART_1:7 .= sup compactbelow x`2 by Th53 .= x`2 by WAYBEL_8:def 3; hence x = sup compactbelow x by A1,A3,DOMAIN_1:12; end; end; definition let S, T be complete algebraic lower-bounded sup-Semilattice; cluster [:S,T:] -> algebraic; coherence proof thus for x being Element of [:S,T:] holds compactbelow x is non empty directed; thus [:S,T:] is up-complete satisfying_axiom_K; end; end; theorem Th69: for S, T being lower-bounded (non empty Poset) st [:S,T:] is algebraic holds S is algebraic & T is algebraic proof let S, T be lower-bounded (non empty Poset) such that A1: for x being Element of [:S,T:] holds compactbelow x is non empty directed and A2: [:S,T:] is up-complete satisfying_axiom_K; A3: S is up-complete & T is up-complete by A2,WAYBEL_2:11; hereby hereby let s be Element of S; consider t being Element of T; A4: [:compactbelow s,compactbelow t:] = compactbelow [s,t] by A3,Th50; A5: proj1 [:compactbelow s,compactbelow t:] = compactbelow s by FUNCT_5:11; compactbelow [s,t] is directed by A1; hence compactbelow s is non empty directed by A4,A5,YELLOW_3:22; end; thus S is up-complete by A2,WAYBEL_2:11; thus S is satisfying_axiom_K proof let s be Element of S; consider t being Element of T; compactbelow [s,t] is non empty directed by A1; then ex_sup_of compactbelow [s,t], [:S,T:] by A2,WAYBEL_0:75; then A6: sup compactbelow [s,t] = [sup proj1 compactbelow [s,t],sup proj2 compactbelow [s,t]] by Th5; thus s = [s,t]`1 by MCART_1:7 .= (sup compactbelow [s,t])`1 by A2,WAYBEL_8:def 3 .= sup proj1 compactbelow [s,t] by A6,MCART_1:7 .= sup compactbelow [s,t]`1 by A3,Th52 .= sup compactbelow s by MCART_1:7; end; end; hereby let t be Element of T; consider s being Element of S; A7: [:compactbelow s,compactbelow t:] = compactbelow [s,t] by A3,Th50; A8: proj2 [:compactbelow s,compactbelow t:] = compactbelow t by FUNCT_5:11; compactbelow [s,t] is directed by A1; hence compactbelow t is non empty directed by A7,A8,YELLOW_3:22; end; thus T is up-complete by A2,WAYBEL_2:11; let t be Element of T; consider s being Element of S; compactbelow [s,t] is non empty directed by A1; then ex_sup_of compactbelow [s,t], [:S,T:] by A2,WAYBEL_0:75; then A9: sup compactbelow [s,t] = [sup proj1 compactbelow [s,t],sup proj2 compactbelow [s,t]] by Th5; thus t = [s,t]`2 by MCART_1:7 .= (sup compactbelow [s,t])`2 by A2,WAYBEL_8:def 3 .= sup proj2 compactbelow [s,t] by A9,MCART_1:7 .= sup compactbelow [s,t]`2 by A3,Th53 .= sup compactbelow t by MCART_1:7; end; definition let S, T be arithmetic lower-bounded LATTICE; cluster [:S,T:] -> arithmetic; coherence proof thus [:S,T:] is algebraic; set C = CompactSublatt [:S,T:]; let x, y be Element of [:S,T:] such that A1: x in the carrier of C & y in the carrier of C & ex_inf_of {x,y},[:S,T:]; A2: CompactSublatt S is meet-inheriting & CompactSublatt T is meet-inheriting by WAYBEL_8:def 5; A3: ex_inf_of {x`1,y`1},S & ex_inf_of {x`2,y`2},T by YELLOW_0:21; x is compact & y is compact by A1,WAYBEL_8:def 1; then x`1 is compact & y`1 is compact & x`2 is compact & y`2 is compact by Th22; then x`1 in the carrier of CompactSublatt S & y`1 in the carrier of CompactSublatt S & x`2 in the carrier of CompactSublatt T & y`2 in the carrier of CompactSublatt T by WAYBEL_8:def 1; then inf {x`1,y`1} in the carrier of CompactSublatt S & inf {x`2,y`2} in the carrier of CompactSublatt T by A2,A3,YELLOW_0:def 16; then x`1 "/\" y`1 in the carrier of CompactSublatt S & x`2 "/\" y`2 in the carrier of CompactSublatt T by YELLOW_0:40; then x`1 "/\" y`1 is compact & x`2 "/\" y`2 is compact by WAYBEL_8:def 1; then (x "/\" y)`1 is compact & (x "/\" y)`2 is compact by Th13; then x "/\" y is compact by Th23; then inf {x,y} is compact by YELLOW_0:40; hence inf {x,y} in the carrier of C by WAYBEL_8:def 1; end; end; theorem for S, T being lower-bounded LATTICE st [:S,T:] is arithmetic holds S is arithmetic & T is arithmetic proof let S, T be lower-bounded LATTICE such that A1: [:S,T:] is algebraic and A2: CompactSublatt [:S,T:] is meet-inheriting; [:S,T:] is up-complete by A1,WAYBEL_8:def 4; then A3: S is up-complete & T is up-complete by WAYBEL_2:11; hereby thus S is algebraic by A1,Th69; let x, y be Element of S such that A4: x in the carrier of CompactSublatt S & y in the carrier of CompactSublatt S and ex_inf_of {x,y},S; A5: ex_inf_of {[x,Bottom T], [y,Bottom T]}, [:S,T:] by YELLOW_0:21; A6: Bottom T is compact by WAYBEL_3:15; A7: [x,Bottom T]`1 = x & [y,Bottom T]`1 = y & [x,Bottom T]`2 = Bottom T & [y, Bottom T]`2 = Bottom T by MCART_1:7; x is compact & y is compact by A4,WAYBEL_8:def 1; then [x,Bottom T] is compact & [y,Bottom T] is compact by A3,A6,A7,Th23; then [x,Bottom T] in the carrier of CompactSublatt [:S,T:] & [y,Bottom T] in the carrier of CompactSublatt [:S,T:] by WAYBEL_8:def 1; then inf {[x,Bottom T], [y,Bottom T]} in the carrier of CompactSublatt [:S,T:] by A2,A5,YELLOW_0:def 16; then A8: inf {[x,Bottom T], [y,Bottom T]} is compact by WAYBEL_8:def 1; (inf {[x,Bottom T], [y,Bottom T]})`1 = ([x,Bottom T] "/\" [y,Bottom T])`1 by YELLOW_0:40 .= [x,Bottom T]`1 "/\" [y,Bottom T]`1 by Th13 .= x "/\" [y,Bottom T]`1 by MCART_1:7 .= x "/\" y by MCART_1:7; then x "/\" y is compact by A3,A8,Th22; then inf {x,y} is compact by YELLOW_0:40; hence inf {x,y} in the carrier of CompactSublatt S by WAYBEL_8:def 1; end; thus T is algebraic by A1,Th69; let x, y be Element of T such that A9: x in the carrier of CompactSublatt T & y in the carrier of CompactSublatt T and ex_inf_of {x,y},T; A10: ex_inf_of {[Bottom S,x], [Bottom S,y]}, [:S,T:] by YELLOW_0:21; A11: Bottom S is compact by WAYBEL_3:15; A12: [Bottom S,x]`2 = x & [Bottom S,y]`2 = y & [Bottom S,x]`1 = Bottom S & [ Bottom S,y]`1 = Bottom S by MCART_1:7; x is compact & y is compact by A9,WAYBEL_8:def 1; then [Bottom S,x] is compact & [Bottom S,y] is compact by A3,A11,A12,Th23; then [Bottom S,x] in the carrier of CompactSublatt [:S,T:] & [Bottom S,y] in the carrier of CompactSublatt [:S,T:] by WAYBEL_8:def 1; then inf {[Bottom S,x], [Bottom S,y]} in the carrier of CompactSublatt [:S ,T:] by A2,A10,YELLOW_0:def 16; then A13: inf {[Bottom S,x], [Bottom S,y]} is compact by WAYBEL_8:def 1; (inf {[Bottom S,x], [Bottom S,y]})`2 = ([Bottom S,x] "/\" [Bottom S,y])`2 by YELLOW_0:40 .= [Bottom S,x]`2 "/\" [Bottom S,y]`2 by Th13 .= x "/\" [Bottom S,y]`2 by MCART_1:7 .= x "/\" y by MCART_1:7; then x "/\" y is compact by A3,A13,Th22; then inf {x,y} is compact by YELLOW_0:40; hence inf {x,y} in the carrier of CompactSublatt T by WAYBEL_8:def 1; end;