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;