:: The Properties of Product of Relational Structures
:: by Artur Korni{\l}owicz
::
:: Received March 27, 1998
:: Copyright (c) 1998-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, LATTICES, ORDERS_2, ZFMISC_1, STRUCT_0, TARSKI,
SUBSET_1, LATTICE3, RELAT_2, XXREAL_0, YELLOW_0, REWRITE1, ORDINAL2,
RELAT_1, MCART_1, EQREL_1, XXREAL_2, WAYBEL_0, WAYBEL_3, RCOMP_1,
WAYBEL_8, WAYBEL_6, CARD_FIL, WAYBEL11, WAYBEL_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, DOMAIN_1, STRUCT_0, MCART_1,
ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_1, YELLOW_3, YELLOW_4,
WAYBEL_2, WAYBEL_3, WAYBEL_6, WAYBEL_8, WAYBEL11;
constructors DOMAIN_1, WAYBEL_1, YELLOW_4, WAYBEL_3, WAYBEL_6, WAYBEL_8,
WAYBEL11, WAYBEL_2, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0,
YELLOW_3, YELLOW_4, WAYBEL_2, WAYBEL_3, WAYBEL_8, WAYBEL14, RELAT_1,
XTUPLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, YELLOW_0, LATTICE3, WAYBEL_0, WAYBEL_1, WAYBEL_2,
WAYBEL_3, WAYBEL_6, WAYBEL_8, WAYBEL11, XBOOLE_0;
equalities YELLOW_0, WAYBEL_3, WAYBEL_8;
expansions YELLOW_0, LATTICE3, WAYBEL_1, WAYBEL_3, WAYBEL_8;
theorems ZFMISC_1, TARSKI, ORDERS_2, YELLOW_0, YELLOW_3, YELLOW_4, WAYBEL_0,
WAYBEL_1, WAYBEL_2, WAYBEL_3, WAYBEL_8, MCART_1, FUNCT_5, DOMAIN_1,
XBOOLE_0, XTUPLE_0;
begin :: On the elements of product of relational structures
registration
let S, T be non empty upper-bounded RelStr;
cluster [:S,T:] -> upper-bounded;
coherence
proof
A1: the carrier of T c= the carrier of T;
consider t being Element of T such that
A2: t is_>=_than the carrier of T by YELLOW_0:def 5;
consider s being Element of S such that
A3: s is_>=_than the carrier of S by YELLOW_0:def 5;
take [s,t];
the carrier of [:S,T:] = [:the carrier of S, the carrier of T:] & the
carrier of S c= the carrier of S by YELLOW_3:def 2;
hence thesis by A3,A2,A1,YELLOW_3:30;
end;
end;
registration
let S, T be non empty lower-bounded RelStr;
cluster [:S,T:] -> lower-bounded;
coherence
proof
A1: the carrier of T c= the carrier of T;
consider t being Element of T such that
A2: t is_<=_than the carrier of T by YELLOW_0:def 4;
consider s being Element of S such that
A3: s is_<=_than the carrier of S by YELLOW_0:def 4;
take [s,t];
the carrier of [:S,T:] = [:the carrier of S, the carrier of T:] & the
carrier of S c= the carrier of S by YELLOW_3:def 2;
hence thesis by A3,A2,A1,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 object such that
A2: s in the carrier of S and
A3: t in the carrier of T and
A4: x = [s,t] by ZFMISC_1:def 2;
reconsider t as Element of T by A3;
reconsider s as Element of S by A2;
A5: the carrier of S c= the carrier of S & the carrier of T c= the carrier
of T;
A6: [s,t] is_>=_than [:the carrier of S,the carrier of T:] by A1,A4;
thus S is upper-bounded
proof
take s;
thus thesis by A5,A6,YELLOW_3:29;
end;
take t;
thus thesis by A5,A6,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 object such that
A2: s in the carrier of S and
A3: t in the carrier of T and
A4: x = [s,t] by ZFMISC_1:def 2;
reconsider t as Element of T by A3;
reconsider s as Element of S by A2;
A5: the carrier of S c= the carrier of S & the carrier of T c= the carrier
of T;
A6: [s,t] is_<=_than [:the carrier of S,the carrier of T:] by A1,A4;
thus S is lower-bounded
proof
take s;
thus thesis by A5,A6,YELLOW_3:32;
end;
take t;
thus thesis by A5,A6,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: 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 object such that
A2: s in the carrier of S and
A3: t in the carrier of T and
A4: a = [s,t] by ZFMISC_1:def 2;
reconsider t as Element of T by A3;
reconsider s as Element of S by A2;
s <= Top S & t <= Top T by YELLOW_0:45;
hence thesis by A4,YELLOW_3:11;
end;
ex_inf_of {},[:S,T:] & {} is_>=_than [Top S,Top T] by YELLOW_0:43;
hence thesis by A1,YELLOW_0:def 10;
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: 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 object such that
A2: s in the carrier of S and
A3: t in the carrier of T and
A4: a = [s,t] by ZFMISC_1:def 2;
reconsider t as Element of T by A3;
reconsider s as Element of S by A2;
Bottom S <= s & Bottom T <= t by YELLOW_0:44;
hence thesis by A4,YELLOW_3:11;
end;
ex_sup_of {},[:S,T:] & {} is_<=_than [Bottom S,Bottom T] by YELLOW_0:42;
hence thesis by A1,YELLOW_0:def 9;
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;
end;
suppose
A2: D = {};
then
A3: sup proj2 D = Bottom T;
sup D = Bottom [:S,T:] & sup proj1 D = Bottom S by A2;
hence thesis by A3,Th4;
end;
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;
end;
suppose
A2: D = {};
then
A3: inf proj2 D = Top T;
inf D = Top [:S,T:] & inf proj1 D = Top S by A2;
hence thesis by A3,Th3;
end;
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
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:21;
y = [y`1,y`2] by A1,MCART_1:21;
then
A3: [y`1,y`2] in {y} by TARSKI:def 1;
assume for b being Element of [:S,T:] st b in {y} holds x <= b;
then
A4: x <= [y`1,y`2] by A3;
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 A4,A2,YELLOW_3:11;
end;
let b be Element of T;
assume b in {y`2};
then b = y`2 by TARSKI:def 1;
hence thesis by A4,A2,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
A7: b = y by TARSKI:def 1;
then b`2 in {y`2} by TARSKI:def 1;
then
A8: x`2 <= b`2 by A6;
b`1 in {y`1} by A7,TARSKI:def 1;
then x`1 <= b`1 by A5;
hence thesis by A8,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] by MCART_1:21;
then [y`1,y`2] in {y,z} by TARSKI:def 2;
then
A3: x <= [y`1,y`2] by A1;
z = [z`1,z`2] by A2,MCART_1:21;
then [z`1,z`2] in {y,z} by TARSKI:def 2;
then
A4: x <= [z`1,z`2] by A1;
A5: x = [x`1,x`2] by A2,MCART_1:21;
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,A5,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 thesis by A3,A4,A5,YELLOW_3:11;
end;
assume that
A6: for b being Element of S st b in {y`1,z`1} holds x`1 <= b and
A7: 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
A8: b = y or b = z by TARSKI:def 2;
then b`2 in {y`2,z`2} by TARSKI:def 2;
then
A9: x`2 <= b`2 by A7;
b`1 in {y`1,z`1} by A8,TARSKI:def 2;
then x`1 <= b`1 by A6;
hence thesis by A9,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
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:21;
y = [y`1,y`2] by A1,MCART_1:21;
then
A3: [y`1,y`2] in {y} by TARSKI:def 1;
assume for b being Element of [:S,T:] st b in {y} holds x >= b;
then
A4: x >= [y`1,y`2] by A3;
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 A4,A2,YELLOW_3:11;
end;
let b be Element of T;
assume b in {y`2};
then b = y`2 by TARSKI:def 1;
hence thesis by A4,A2,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
A7: b = y by TARSKI:def 1;
then b`2 in {y`2} by TARSKI:def 1;
then
A8: x`2 >= b`2 by A6;
b`1 in {y`1} by A7,TARSKI:def 1;
then x`1 >= b`1 by A5;
hence thesis by A8,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] by MCART_1:21;
then [y`1,y`2] in {y,z} by TARSKI:def 2;
then
A3: x >= [y`1,y`2] by A1;
z = [z`1,z`2] by A2,MCART_1:21;
then [z`1,z`2] in {y,z} by TARSKI:def 2;
then
A4: x >= [z`1,z`2] by A1;
A5: x = [x`1,x`2] by A2,MCART_1:21;
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,A5,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 thesis by A3,A4,A5,YELLOW_3:11;
end;
assume that
A6: for b being Element of S st b in {y`1,z`1} holds x`1 >= b and
A7: 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
A8: b = y or b = z by TARSKI:def 2;
then b`2 in {y`2,z`2} by TARSKI:def 2;
then
A9: x`2 >= b`2 by A7;
b`1 in {y`1,z`1} by A8,TARSKI:def 2;
then x`1 >= b`1 by A6;
hence thesis by A9,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:21;
then proj1 {x,y} = {x`1,y`1} & proj2 {x,y} = {x`2,y`2} by FUNCT_5:13;
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:21;
then proj1 {x,y} = {x`1,y`1} & proj2 {x,y} = {x`2,y`2} by FUNCT_5:13;
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:];
set a = (x "/\" y)`1, b = (x "/\" y)`2;
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:21;
A3: y = [y`1,y`2] by A1,MCART_1:21;
A4: for d being Element of S st d <= x`1 & d <= y`1 holds a >= d
proof
set t = x`2 "/\" y`2;
let d be Element of S such that
A5: d <= x`1 and
A6: d <= y`1;
t <= y`2 by YELLOW_0:23;
then
A7: [d,t] <= y by A3,A6,YELLOW_3:11;
t <= x`2 by YELLOW_0:23;
then [d,t] <= x by A2,A5,YELLOW_3:11;
then
A8: x "/\" y >= [d,t] by A7,YELLOW_0:23;
[d,t]`1 = d;
hence thesis by A8,YELLOW_3:12;
end;
A9: for d being Element of T st d <= x`2 & d <= y`2 holds b >= d
proof
set s = x`1 "/\" y`1;
let d be Element of T such that
A10: d <= x`2 and
A11: d <= y`2;
s <= y`1 by YELLOW_0:23;
then
A12: [s,d] <= y by A3,A11,YELLOW_3:11;
s <= x`1 by YELLOW_0:23;
then [s,d] <= x by A2,A10,YELLOW_3:11;
then
A13: x "/\" y >= [s,d] by A12,YELLOW_0:23;
[s,d]`2 = d;
hence thesis by A13,YELLOW_3:12;
end;
x "/\" y <= y by YELLOW_0:23;
then
A14: a <= y`1 & b <= y`2 by YELLOW_3:12;
x "/\" y <= x by YELLOW_0:23;
then a <= x`1 & b <= x`2 by YELLOW_3:12;
hence thesis by A14,A4,A9,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:];
set a = (x "\/" y)`1, b = (x "\/" y)`2;
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:21;
A3: y = [y`1,y`2] by A1,MCART_1:21;
A4: for d being Element of S st d >= x`1 & d >= y`1 holds a <= d
proof
set t = x`2 "\/" y`2;
let d be Element of S such that
A5: d >= x`1 and
A6: d >= y`1;
t >= y`2 by YELLOW_0:22;
then
A7: [d,t] >= y by A3,A6,YELLOW_3:11;
t >= x`2 by YELLOW_0:22;
then [d,t] >= x by A2,A5,YELLOW_3:11;
then
A8: x "\/" y <= [d,t] by A7,YELLOW_0:22;
[d,t]`1 = d;
hence thesis by A8,YELLOW_3:12;
end;
A9: for d being Element of T st d >= x`2 & d >= y`2 holds b <= d
proof
set s = x`1 "\/" y`1;
let d be Element of T such that
A10: d >= x`2 and
A11: d >= y`2;
s >= y`1 by YELLOW_0:22;
then
A12: [s,d] >= y by A3,A11,YELLOW_3:11;
s >= x`1 by YELLOW_0:22;
then [s,d] >= x by A2,A10,YELLOW_3:11;
then
A13: x "\/" y <= [s,d] by A12,YELLOW_0:22;
[s,d]`2 = d;
hence thesis by A13,YELLOW_3:12;
end;
x "\/" y >= y by YELLOW_0:22;
then
A14: a >= y`1 & b >= y`2 by YELLOW_3:12;
x "\/" y >= x by YELLOW_0:22;
then a >= x`1 & b >= x`2 by YELLOW_3:12;
hence thesis by A14,A4,A9,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])`2 = [x1,x2]`2 "/\" [y1,y2]`2 by Th13
.= x2 "/\" [y1,y2]`2
.= x2 "/\" y2
.= [x1 "/\" y1, x2 "/\" y2]`2;
([x1,x2] "/\" [y1,y2])`1 = [x1,x2]`1 "/\" [y1,y2]`1 by Th13
.= x1 "/\" [y1,y2]`1
.= x1 "/\" y1
.= [x1 "/\" y1, x2 "/\" y2]`1;
hence thesis by A1,A2,DOMAIN_1:2;
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])`2 = [x1,x2]`2 "\/" [y1,y2]`2 by Th14
.= x2 "\/" [y1,y2]`2
.= x2 "\/" y2
.= [x1 "\/" y1, x2 "\/" y2]`2;
([x1,x2] "\/" [y1,y2])`1 = [x1,x2]`1 "\/" [y1,y2]`1 by Th14
.= x1 "\/" [y1,y2]`1
.= x1 "\/" y1
.= [x1 "\/" y1, x2 "\/" y2]`1;
hence thesis by A1,A2,DOMAIN_1:2;
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; :: redefines is_a_complement_of (WAYBEL_1, definition)
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;
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:];
A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by
YELLOW_3:def 2;
hereby
assume
A2: x is_a_complement_of y;
A3: y`1 "/\" x`1 = (y "/\" x)`1 by Th13
.= (Bottom [:S,T:])`1 by A2
.= [Bottom S,Bottom T]`1 by Th4
.= Bottom S;
y`1 "\/" x`1 = (y "\/" x)`1 by Th14
.= (Top [:S,T:])`1 by A2
.= [Top S,Top T]`1 by Th3
.= Top S;
hence x`1 is_a_complement_of y`1 by A3;
A4: y`2 "/\" x`2 = (y "/\" x)`2 by Th13
.= (Bottom [:S,T:])`2 by A2
.= [Bottom S,Bottom T]`2 by Th4
.= Bottom T;
y`2 "\/" x`2 = (y "\/" x)`2 by Th14
.= (Top [:S,T:])`2 by A2
.= [Top S,Top T]`2 by Th3
.= Top T;
hence x`2 is_a_complement_of y`2 by A4;
end;
assume that
A5: y`1 "\/" x`1 = Top S and
A6: y`1 "/\" x`1 = Bottom S and
A7: y`2 "\/" x`2 = Top T and
A8: y`2 "/\" x`2 = Bottom T;
A9: (y "\/" x)`2 = y`2 "\/" x`2 by Th14
.= [Top S,Top T]`2 by A7;
(y "\/" x)`1 = y`1 "\/" x`1 by Th14
.= [Top S,Top T]`1 by A5;
hence y "\/" x = [Top S,Top T] by A1,A9,DOMAIN_1:2
.= Top [:S,T:] by Th3;
A10: (y "/\" x)`2 = y`2 "/\" x`2 by Th13
.= [Bottom S,Bottom T]`2 by A8;
(y "/\" x)`1 = y`1 "/\" x`1 by Th13
.= [Bottom S,Bottom T]`1 by A6;
hence y "/\" x = [Bottom S,Bottom T] by A1,A10,DOMAIN_1:2
.= 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;
assume
A1: 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;
A2: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by
YELLOW_3:def 2;
thus a << c
proof
reconsider d9 = {d} as non empty directed Subset of T by WAYBEL_0:5;
let D be non empty directed Subset of S such that
A3: c <= sup D;
A4: d <= sup d9 by YELLOW_0:39;
ex_sup_of D,S & ex_sup_of d9,T by WAYBEL_0:75;
then sup [:D,d9:] = [sup D,sup d9] by YELLOW_3:43;
then [c,d] <= sup [:D,d9:] by A3,A4,YELLOW_3:11;
then consider e being Element of [:S,T:] such that
A5: e in [:D,d9:] and
A6: [a,b] <= e by A1;
take e`1;
thus e`1 in D by A5,MCART_1:10;
e = [e`1,e`2] by A2,MCART_1:21;
hence thesis by A6,YELLOW_3:11;
end;
let D be non empty directed Subset of T such that
A7: d <= sup D;
reconsider c9 = {c} as non empty directed Subset of S by WAYBEL_0:5;
A8: c <= sup c9 by YELLOW_0:39;
ex_sup_of c9,S & ex_sup_of D,T by WAYBEL_0:75;
then sup [:c9,D:] = [sup c9,sup D] by YELLOW_3:43;
then [c,d] <= sup [:c9,D:] by A7,A8,YELLOW_3:11;
then consider e being Element of [:S,T:] such that
A9: e in [:c9,D:] and
A10: [a,b] <= e by A1;
take e`2;
thus e`2 in D by A9,MCART_1:10;
e = [e`1,e`2] by A2,MCART_1:21;
hence thesis by A10,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;
assume
A1: 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
A2: 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
A3: [c,d] <= sup D;
ex_sup_of D,[:S,T:] by WAYBEL_0:75;
then
A4: sup D = [sup proj1 D,sup proj2 D] by YELLOW_3:46;
then proj1 D is non empty directed & c <= sup proj1 D by A3,YELLOW_3:11,21,22
;
then consider e being Element of S such that
A5: e in proj1 D and
A6: a <= e by A1;
consider e2 being object such that
A7: [e,e2] in D by A5,XTUPLE_0:def 12;
proj2 D is non empty directed & d <= sup proj2 D by A3,A4,YELLOW_3:11,21,22;
then consider f being Element of T such that
A8: f in proj2 D and
A9: b <= f by A2;
consider f1 being object such that
A10: [f1,f] in D by A8,XTUPLE_0:def 13;
A11: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by
YELLOW_3:def 2;
then reconsider e2 as Element of T by A7,ZFMISC_1:87;
reconsider f1 as Element of S by A11,A10,ZFMISC_1:87;
consider ef being Element of [:S,T:] such that
A12: ef in D and
A13: [e,e2] <= ef & [f1,f] <= ef by A7,A10,WAYBEL_0:def 1;
A14: ef = [ef`1,ef`2] by A11,MCART_1:21;
then e <= ef`1 & f <= ef`2 by A13,YELLOW_3:11;
then
A15: [e,f] <= ef by A14,YELLOW_3:11;
take ef;
thus ef in D by A12;
[a,b] <= [e,f] by A6,A9,YELLOW_3:11;
hence thesis by A15,ORDERS_2:3;
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:21;
hence thesis 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:21;
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 object;
assume a in proj1 (X "/\" Y);
then consider b being object such that
A4: [a,b] in X "/\" Y by XTUPLE_0:def 12;
consider x, y being Element of [:S,T:] such that
A5: [a,b] = x "/\" y and
A6: x in X and
A7: y in Y by A2,A4;
x = [x`1,x`2] by A1,MCART_1:21;
then
A8: x`1 in proj1 X by A6,XTUPLE_0:def 12;
y = [y`1,y`2] by A1,MCART_1:21;
then
A9: y`1 in proj1 Y by A7,XTUPLE_0:def 12;
a = [a,b]`1
.= x`1 "/\" y`1 by A5,Th13;
hence a in proj1 X "/\" proj1 Y by A8,A9,YELLOW_4:37;
end;
let a be object;
assume a in proj1 X "/\" proj1 Y;
then consider x, y being Element of S such that
A10: a = x "/\" y and
A11: x in proj1 X and
A12: y in proj1 Y by A3;
consider x2 being object such that
A13: [x,x2] in X by A11,XTUPLE_0:def 12;
consider y2 being object such that
A14: [y,y2] in Y by A12,XTUPLE_0:def 12;
reconsider x2, y2 as Element of T by A1,A13,A14,ZFMISC_1:87;
[x,x2] "/\" [y,y2] = [a,x2 "/\" y2] by A10,Th15;
then [a,x2 "/\" y2] in X "/\" Y by A13,A14,YELLOW_4:37;
hence a in proj1 (X "/\" Y) by XTUPLE_0:def 12;
end;
hereby
let b be object;
assume b in proj2 (X "/\" Y);
then consider a being object such that
A15: [a,b] in X "/\" Y by XTUPLE_0:def 13;
consider x, y being Element of [:S,T:] such that
A16: [a,b] = x "/\" y and
A17: x in X and
A18: y in Y by A2,A15;
x = [x`1,x`2] by A1,MCART_1:21;
then
A19: x`2 in proj2 X by A17,XTUPLE_0:def 13;
y = [y`1,y`2] by A1,MCART_1:21;
then
A20: y`2 in proj2 Y by A18,XTUPLE_0:def 13;
b = [a,b]`2
.= x`2 "/\" y`2 by A16,Th13;
hence b in proj2 X "/\" proj2 Y by A19,A20,YELLOW_4:37;
end;
let b be object;
A21: 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;
assume b in proj2 X "/\" proj2 Y;
then consider x, y being Element of T such that
A22: b = x "/\" y and
A23: x in proj2 X and
A24: y in proj2 Y by A21;
consider x1 being object such that
A25: [x1,x] in X by A23,XTUPLE_0:def 13;
consider y1 being object such that
A26: [y1,y] in Y by A24,XTUPLE_0:def 13;
reconsider x1, y1 as Element of S by A1,A25,A26,ZFMISC_1:87;
[x1,x] "/\" [y1,y] = [x1 "/\" y1,b] by A22,Th15;
then [x1 "/\" y1,b] in X "/\" Y by A25,A26,YELLOW_4:37;
hence thesis by XTUPLE_0:def 13;
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 object;
assume a in proj1 (X "\/" Y);
then consider b being object such that
A4: [a,b] in X "\/" Y by XTUPLE_0:def 12;
consider x, y being Element of [:S,T:] such that
A5: [a,b] = x "\/" y and
A6: x in X and
A7: y in Y by A2,A4;
x = [x`1,x`2] by A1,MCART_1:21;
then
A8: x`1 in proj1 X by A6,XTUPLE_0:def 12;
y = [y`1,y`2] by A1,MCART_1:21;
then
A9: y`1 in proj1 Y by A7,XTUPLE_0:def 12;
a = [a,b]`1
.= x`1 "\/" y`1 by A5,Th14;
hence a in proj1 X "\/" proj1 Y by A8,A9,YELLOW_4:10;
end;
let a be object;
assume a in proj1 X "\/" proj1 Y;
then consider x, y being Element of S such that
A10: a = x "\/" y and
A11: x in proj1 X and
A12: y in proj1 Y by A3;
consider x2 being object such that
A13: [x,x2] in X by A11,XTUPLE_0:def 12;
consider y2 being object such that
A14: [y,y2] in Y by A12,XTUPLE_0:def 12;
reconsider x2, y2 as Element of T by A1,A13,A14,ZFMISC_1:87;
[x,x2] "\/" [y,y2] = [a,x2 "\/" y2] by A10,Th16;
then [a,x2 "\/" y2] in X "\/" Y by A13,A14,YELLOW_4:10;
hence a in proj1 (X "\/" Y) by XTUPLE_0:def 12;
end;
hereby
let b be object;
assume b in proj2 (X "\/" Y);
then consider a being object such that
A15: [a,b] in X "\/" Y by XTUPLE_0:def 13;
consider x, y being Element of [:S,T:] such that
A16: [a,b] = x "\/" y and
A17: x in X and
A18: y in Y by A2,A15;
x = [x`1,x`2] by A1,MCART_1:21;
then
A19: x`2 in proj2 X by A17,XTUPLE_0:def 13;
y = [y`1,y`2] by A1,MCART_1:21;
then
A20: y`2 in proj2 Y by A18,XTUPLE_0:def 13;
b = [a,b]`2
.= x`2 "\/" y`2 by A16,Th14;
hence b in proj2 X "\/" proj2 Y by A19,A20,YELLOW_4:10;
end;
let b be object;
A21: 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;
assume b in proj2 X "\/" proj2 Y;
then consider x, y being Element of T such that
A22: b = x "\/" y and
A23: x in proj2 X and
A24: y in proj2 Y by A21;
consider x1 being object such that
A25: [x1,x] in X by A23,XTUPLE_0:def 13;
consider y1 being object such that
A26: [y1,y] in Y by A24,XTUPLE_0:def 13;
reconsider x1, y1 as Element of S by A1,A25,A26,ZFMISC_1:87;
[x1,x] "\/" [y1,y] = [x1 "\/" y1,b] by A22,Th16;
then [x1 "\/" y1,b] in X "\/" Y by A25,A26,YELLOW_4:10;
hence thesis by XTUPLE_0:def 13;
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:];
let x be object;
assume
A1: x in downarrow X;
A2: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by
YELLOW_3:def 2;
then
ex a, b being object st a in the carrier of S & b in the carrier of T & x =
[a,b] by A1,ZFMISC_1:def 2;
then reconsider S9 = S, T9 = T as non empty RelStr;
reconsider x9 = x as Element of [:S9,T9:] by A1;
consider y being Element of [:S9,T9:] such that
A3: y >= x9 and
A4: y in X by A1,WAYBEL_0:def 15;
A5: y`1 >= x9`1 by A3,YELLOW_3:12;
A6: y = [y`1,y`2] by A2,MCART_1:21;
then y`1 in proj1 X by A4,XTUPLE_0:def 12;
then
A7: x`1 in downarrow proj1 X by A5,WAYBEL_0:def 15;
A8: y`2 >= x9`2 by A3,YELLOW_3:12;
y`2 in proj2 X by A4,A6,XTUPLE_0:def 13;
then
A9: x`2 in downarrow proj2 X by A8,WAYBEL_0:def 15;
x9 = [x9`1,x9`2] by A2,MCART_1:21;
hence thesis by A7,A9,ZFMISC_1:def 2;
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;
hereby
let x be object;
assume x in [:downarrow X,downarrow Y:];
then consider x1, x2 being object such that
A1: x1 in downarrow X and
A2: x2 in downarrow Y and
A3: x = [x1,x2] by ZFMISC_1:def 2;
reconsider S9 = S, T9 = T as non empty RelStr by A1,A2;
reconsider x1 as Element of S9 by A1;
consider y1 being Element of S9 such that
A4: y1 >= x1 & y1 in X by A1,WAYBEL_0:def 15;
reconsider x2 as Element of T9 by A2;
consider y2 being Element of T9 such that
A5: y2 >= x2 & y2 in Y by A2,WAYBEL_0:def 15;
[y1,y2] in [:X,Y:] & [y1,y2] >= [x1,x2] by A4,A5,YELLOW_3:11,ZFMISC_1:87;
hence x in downarrow [:X,Y:] by A3,WAYBEL_0:def 15;
end;
let x be object;
assume
A6: x in downarrow [:X,Y:];
A7: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by
YELLOW_3:def 2;
then
ex a, b being object st a in the carrier of S & b in the carrier of T & x =
[a,b] by A6,ZFMISC_1:def 2;
then reconsider S9 = S, T9 = T as non empty RelStr;
reconsider x9 = x as Element of [:S9,T9:] by A6;
consider y being Element of [:S9,T9:] such that
A8: y >= x9 & y in [:X,Y:] by A6,WAYBEL_0:def 15;
y`2 >= x9`2 & y`2 in Y by A8,MCART_1:10,YELLOW_3:12;
then
A9: x`2 in downarrow Y by WAYBEL_0:def 15;
y`1 >= x9`1 & y`1 in X by A8,MCART_1:10,YELLOW_3:12;
then
A10: x`1 in downarrow X by WAYBEL_0:def 15;
x9 = [x9`1,x9`2] by A7,MCART_1:21;
hence thesis by A10,A9,ZFMISC_1:def 2;
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 object;
assume a in proj1 downarrow X;
then consider b being object such that
A2: [a,b] in downarrow X by XTUPLE_0:def 12;
reconsider S9 = S, T9 = T as non empty RelStr by A1,A2,ZFMISC_1:87;
reconsider b9 = b as Element of T9 by A1,A2,ZFMISC_1:87;
reconsider a9 = a as Element of S9 by A1,A2,ZFMISC_1:87;
consider c being Element of [:S9,T9:] such that
A3: [a9,b9] <= c & c in X by A2,WAYBEL_0:def 15;
c = [c`1,c`2] by A1,MCART_1:21;
then a9 <= c`1 & c`1 in proj1 X by A3,XTUPLE_0:def 12,YELLOW_3:11;
hence a in downarrow proj1 X by WAYBEL_0:def 15;
end;
let b be object;
assume b in proj2 downarrow X;
then consider a being object such that
A4: [a,b] in downarrow X by XTUPLE_0:def 13;
reconsider S9 = S, T9 = T as non empty RelStr by A1,A4,ZFMISC_1:87;
reconsider b9 = b as Element of T9 by A1,A4,ZFMISC_1:87;
reconsider a9 = a as Element of S9 by A1,A4,ZFMISC_1:87;
consider c being Element of [:S9,T9:] such that
A5: [a9,b9] <= c & c in X by A4,WAYBEL_0:def 15;
c = [c`1,c`2] by A1,MCART_1:21;
then b9 <= c`2 & c`2 in proj2 X by A5,XTUPLE_0:def 13,YELLOW_3:11;
hence thesis by 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:];
thus proj1 downarrow X c= downarrow proj1 X by Th28;
let a be object;
assume
A1: a in downarrow proj1 X;
then reconsider S9 = S as non empty RelStr;
reconsider a9 = a as Element of S9 by A1;
consider b being Element of S9 such that
A2: b >= a9 and
A3: b in proj1 X by A1,WAYBEL_0:def 15;
consider b2 being object such that
A4: [b,b2] in X by A3,XTUPLE_0:def 12;
A5: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by
YELLOW_3:def 2;
then reconsider T9 = T as non empty reflexive RelStr by A4,ZFMISC_1:87;
reconsider b2 as Element of T9 by A5,A4,ZFMISC_1:87;
b2 <= b2;
then [b,b2] >= [a9,b2] by A2,YELLOW_3:11;
then [a9,b2] in downarrow X by A4,WAYBEL_0:def 15;
hence thesis by XTUPLE_0:def 12;
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:];
thus proj2 downarrow X c= downarrow proj2 X by Th28;
let c be object;
assume
A1: c in downarrow proj2 X;
then reconsider T9 = T as non empty RelStr;
reconsider c9 = c as Element of T9 by A1;
consider b being Element of T9 such that
A2: b >= c9 and
A3: b in proj2 X by A1,WAYBEL_0:def 15;
consider b1 being object such that
A4: [b1,b] in X by A3,XTUPLE_0:def 13;
A5: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by
YELLOW_3:def 2;
then reconsider S9 = S as non empty reflexive RelStr by A4,ZFMISC_1:87;
reconsider b1 as Element of S9 by A5,A4,ZFMISC_1:87;
b1 <= b1;
then [b1,b] >= [b1,c9] by A2,YELLOW_3:11;
then [b1,c9] in downarrow X by A4,WAYBEL_0:def 15;
hence thesis by XTUPLE_0:def 13;
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:];
let x be object;
assume
A1: x in uparrow X;
A2: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by
YELLOW_3:def 2;
then
ex a, b being object st a in the carrier of S & b in the carrier of T & x =
[a,b] by A1,ZFMISC_1:def 2;
then reconsider S9 = S, T9 = T as non empty RelStr;
reconsider x9 = x as Element of [:S9,T9:] by A1;
consider y being Element of [:S9,T9:] such that
A3: y <= x9 and
A4: y in X by A1,WAYBEL_0:def 16;
A5: y`1 <= x9`1 by A3,YELLOW_3:12;
A6: y = [y`1,y`2] by A2,MCART_1:21;
then y`1 in proj1 X by A4,XTUPLE_0:def 12;
then
A7: x`1 in uparrow proj1 X by A5,WAYBEL_0:def 16;
A8: y`2 <= x9`2 by A3,YELLOW_3:12;
y`2 in proj2 X by A4,A6,XTUPLE_0:def 13;
then
A9: x`2 in uparrow proj2 X by A8,WAYBEL_0:def 16;
x9 = [x9`1,x9`2] by A2,MCART_1:21;
hence thesis by A7,A9,ZFMISC_1:def 2;
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;
hereby
let x be object;
assume x in [:uparrow X,uparrow Y:];
then consider x1, x2 being object such that
A1: x1 in uparrow X and
A2: x2 in uparrow Y and
A3: x = [x1,x2] by ZFMISC_1:def 2;
reconsider S9 = S, T9 = T as non empty RelStr by A1,A2;
reconsider x1 as Element of S9 by A1;
consider y1 being Element of S9 such that
A4: y1 <= x1 & y1 in X by A1,WAYBEL_0:def 16;
reconsider x2 as Element of T9 by A2;
consider y2 being Element of T9 such that
A5: y2 <= x2 & y2 in Y by A2,WAYBEL_0:def 16;
[y1,y2] in [:X,Y:] & [y1,y2] <= [x1,x2] by A4,A5,YELLOW_3:11,ZFMISC_1:87;
hence x in uparrow [:X,Y:] by A3,WAYBEL_0:def 16;
end;
let x be object;
assume
A6: x in uparrow [:X,Y:];
A7: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by
YELLOW_3:def 2;
then
ex a, b being object st a in the carrier of S & b in the carrier of T & x =
[a,b] by A6,ZFMISC_1:def 2;
then reconsider S9 = S, T9 = T as non empty RelStr;
reconsider x9 = x as Element of [:S9,T9:] by A6;
consider y being Element of [:S9,T9:] such that
A8: y <= x9 & y in [:X,Y:] by A6,WAYBEL_0:def 16;
y`2 <= x9`2 & y`2 in Y by A8,MCART_1:10,YELLOW_3:12;
then
A9: x`2 in uparrow Y by WAYBEL_0:def 16;
y`1 <= x9`1 & y`1 in X by A8,MCART_1:10,YELLOW_3:12;
then
A10: x`1 in uparrow X by WAYBEL_0:def 16;
x9 = [x9`1,x9`2] by A7,MCART_1:21;
hence thesis by A10,A9,ZFMISC_1:def 2;
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 object;
assume a in proj1 uparrow X;
then consider b being object such that
A2: [a,b] in uparrow X by XTUPLE_0:def 12;
reconsider S9 = S, T9 = T as non empty RelStr by A1,A2,ZFMISC_1:87;
reconsider b9 = b as Element of T9 by A1,A2,ZFMISC_1:87;
reconsider a9 = a as Element of S9 by A1,A2,ZFMISC_1:87;
consider c being Element of [:S9,T9:] such that
A3: [a9,b9] >= c & c in X by A2,WAYBEL_0:def 16;
c = [c`1,c`2] by A1,MCART_1:21;
then a9 >= c`1 & c`1 in proj1 X by A3,XTUPLE_0:def 12,YELLOW_3:11;
hence a in uparrow proj1 X by WAYBEL_0:def 16;
end;
let b be object;
assume b in proj2 uparrow X;
then consider a being object such that
A4: [a,b] in uparrow X by XTUPLE_0:def 13;
reconsider S9 = S, T9 = T as non empty RelStr by A1,A4,ZFMISC_1:87;
reconsider b9 = b as Element of T9 by A1,A4,ZFMISC_1:87;
reconsider a9 = a as Element of S9 by A1,A4,ZFMISC_1:87;
consider c being Element of [:S9,T9:] such that
A5: [a9,b9] >= c & c in X by A4,WAYBEL_0:def 16;
c = [c`1,c`2] by A1,MCART_1:21;
then b9 >= c`2 & c`2 in proj2 X by A5,XTUPLE_0:def 13,YELLOW_3:11;
hence thesis by 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:];
thus proj1 uparrow X c= uparrow proj1 X by Th33;
let a be object;
assume
A1: a in uparrow proj1 X;
then reconsider S9 = S as non empty RelStr;
reconsider a9 = a as Element of S9 by A1;
consider b being Element of S9 such that
A2: b <= a9 and
A3: b in proj1 X by A1,WAYBEL_0:def 16;
consider b2 being object such that
A4: [b,b2] in X by A3,XTUPLE_0:def 12;
A5: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by
YELLOW_3:def 2;
then reconsider T9 = T as non empty reflexive RelStr by A4,ZFMISC_1:87;
reconsider b2 as Element of T9 by A5,A4,ZFMISC_1:87;
b2 <= b2;
then [b,b2] <= [a9,b2] by A2,YELLOW_3:11;
then [a9,b2] in uparrow X by A4,WAYBEL_0:def 16;
hence thesis by XTUPLE_0:def 12;
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:];
thus proj2 uparrow X c= uparrow proj2 X by Th33;
let c be object;
assume
A1: c in uparrow proj2 X;
then reconsider T9 = T as non empty RelStr;
reconsider c9 = c as Element of T9 by A1;
consider b being Element of T9 such that
A2: b <= c9 and
A3: b in proj2 X by A1,WAYBEL_0:def 16;
consider b1 being object such that
A4: [b1,b] in X by A3,XTUPLE_0:def 13;
A5: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by
YELLOW_3:def 2;
then reconsider S9 = S as non empty reflexive RelStr by A4,ZFMISC_1:87;
reconsider b1 as Element of S9 by A5,A4,ZFMISC_1:87;
b1 <= b1;
then [b1,b] <= [b1,c9] by A2,YELLOW_3:11;
then [b1,c9] in uparrow X by A4,WAYBEL_0:def 16;
hence thesis by XTUPLE_0:def 13;
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;
hereby
let x be object;
assume x in [:downarrow s,downarrow t:];
then consider x1, x2 being object such that
A1: x1 in downarrow s and
A2: x2 in downarrow t and
A3: x = [x1,x2] by ZFMISC_1:def 2;
reconsider x2 as Element of T by A2;
reconsider x1 as Element of S by A1;
s >= x1 & t >= x2 by A1,A2,WAYBEL_0:17;
then [s,t] >= [x1,x2] by YELLOW_3:11;
hence x in downarrow [s,t] by A3,WAYBEL_0:17;
end;
let x be object;
assume
A4: x in downarrow [s,t];
then reconsider x9 = x as Element of [:S,T:];
the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by
YELLOW_3:def 2;
then
A5: x9 = [x9`1,x9`2] by MCART_1:21;
A6: [s,t] >= x9 by A4,WAYBEL_0:17;
then t >= x9`2 by A5,YELLOW_3:11;
then
A7: x`2 in downarrow t by WAYBEL_0:17;
s >= x9`1 by A5,A6,YELLOW_3:11;
then x`1 in downarrow s by WAYBEL_0:17;
hence thesis by A5,A7,ZFMISC_1:def 2;
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:21;
hereby
let a be object;
assume a in proj1 downarrow x;
then consider b being object such that
A3: [a,b] in downarrow x by XTUPLE_0:def 12;
reconsider b as Element of T by A1,A3,ZFMISC_1:87;
reconsider a9 = a as Element of S by A1,A3,ZFMISC_1:87;
[a9,b] <= x by A3,WAYBEL_0:17;
then a9 <= x`1 by A2,YELLOW_3:11;
hence a in downarrow x`1 by WAYBEL_0:17;
end;
let b be object;
assume b in proj2 downarrow x;
then consider a being object such that
A4: [a,b] in downarrow x by XTUPLE_0:def 13;
reconsider a as Element of S by A1,A4,ZFMISC_1:87;
reconsider b9 = b as Element of T by A1,A4,ZFMISC_1:87;
[a,b9] <= x by A4,WAYBEL_0:17;
then b9 <= x`2 by A2,YELLOW_3:11;
hence thesis 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:];
A1: x`2 <= x`2;
thus proj1 downarrow x c= downarrow x`1 by Th37;
let a be object;
assume
A2: a in downarrow x`1;
then reconsider a9 = a as Element of S;
a9 <= x`1 by A2,WAYBEL_0:17;
then [a9,x`2] <= [x`1,x`2] by A1,YELLOW_3:11;
then
A3: [a9,x`2] in downarrow [x`1,x`2] by WAYBEL_0:17;
the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by
YELLOW_3:def 2;
then x = [x`1,x`2] by MCART_1:21;
hence thesis by A3,XTUPLE_0:def 12;
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:];
A1: x`1 <= x`1;
thus proj2 downarrow x c= downarrow x`2 by Th37;
let b be object;
assume
A2: b in downarrow x`2;
then reconsider b9 = b as Element of T;
b9 <= x`2 by A2,WAYBEL_0:17;
then [x`1,b9] <= [x`1,x`2] by A1,YELLOW_3:11;
then
A3: [x`1,b9] in downarrow [x`1,x`2] by WAYBEL_0:17;
the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by
YELLOW_3:def 2;
then x = [x`1,x`2] by MCART_1:21;
hence thesis by A3,XTUPLE_0:def 13;
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;
hereby
let x be object;
assume x in [:uparrow s,uparrow t:];
then consider x1, x2 being object such that
A1: x1 in uparrow s and
A2: x2 in uparrow t and
A3: x = [x1,x2] by ZFMISC_1:def 2;
reconsider x2 as Element of T by A2;
reconsider x1 as Element of S by A1;
s <= x1 & t <= x2 by A1,A2,WAYBEL_0:18;
then [s,t] <= [x1,x2] by YELLOW_3:11;
hence x in uparrow [s,t] by A3,WAYBEL_0:18;
end;
let x be object;
assume
A4: x in uparrow [s,t];
then reconsider x9 = x as Element of [:S,T:];
the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by
YELLOW_3:def 2;
then
A5: x9 = [x9`1,x9`2] by MCART_1:21;
A6: [s,t] <= x9 by A4,WAYBEL_0:18;
then t <= x9`2 by A5,YELLOW_3:11;
then
A7: x`2 in uparrow t by WAYBEL_0:18;
s <= x9`1 by A5,A6,YELLOW_3:11;
then x`1 in uparrow s by WAYBEL_0:18;
hence thesis by A5,A7,ZFMISC_1:def 2;
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:21;
hereby
let a be object;
assume a in proj1 uparrow x;
then consider b being object such that
A3: [a,b] in uparrow x by XTUPLE_0:def 12;
reconsider b as Element of T by A1,A3,ZFMISC_1:87;
reconsider a9 = a as Element of S by A1,A3,ZFMISC_1:87;
[a9,b] >= x by A3,WAYBEL_0:18;
then a9 >= x`1 by A2,YELLOW_3:11;
hence a in uparrow x`1 by WAYBEL_0:18;
end;
let b be object;
assume b in proj2 uparrow x;
then consider a being object such that
A4: [a,b] in uparrow x by XTUPLE_0:def 13;
reconsider a as Element of S by A1,A4,ZFMISC_1:87;
reconsider b9 = b as Element of T by A1,A4,ZFMISC_1:87;
[a,b9] >= x by A4,WAYBEL_0:18;
then b9 >= x`2 by A2,YELLOW_3:11;
hence thesis 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:];
A1: x`2 <= x`2;
thus proj1 uparrow x c= uparrow x`1 by Th41;
let a be object;
assume
A2: a in uparrow x`1;
then reconsider a9 = a as Element of S;
a9 >= x`1 by A2,WAYBEL_0:18;
then [a9,x`2] >= [x`1,x`2] by A1,YELLOW_3:11;
then
A3: [a9,x`2] in uparrow [x`1,x`2] by WAYBEL_0:18;
the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by
YELLOW_3:def 2;
then x = [x`1,x`2] by MCART_1:21;
hence thesis by A3,XTUPLE_0:def 12;
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:];
A1: x`1 <= x`1;
thus proj2 uparrow x c= uparrow x`2 by Th41;
let b be object;
assume
A2: b in uparrow x`2;
then reconsider b9 = b as Element of T;
b9 >= x`2 by A2,WAYBEL_0:18;
then [x`1,b9] >= [x`1,x`2] by A1,YELLOW_3:11;
then
A3: [x`1,b9] in uparrow [x`1,x`2] by WAYBEL_0:18;
the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by
YELLOW_3:def 2;
then x = [x`1,x`2] by MCART_1:21;
hence thesis by A3,XTUPLE_0:def 13;
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;
hereby
let x be object;
assume x in [:waybelow s,waybelow t:];
then consider x1, x2 being object such that
A1: x1 in waybelow s and
A2: x2 in waybelow t and
A3: x = [x1,x2] by ZFMISC_1:def 2;
reconsider x2 as Element of T by A2;
reconsider x1 as Element of S by A1;
s >> x1 & t >> x2 by A1,A2,WAYBEL_3:7;
then [s,t] >> [x1,x2] by Th19;
hence x in waybelow [s,t] by A3;
end;
let x be object;
assume
A4: x in waybelow [s,t];
then reconsider x9 = x as Element of [:S,T:];
the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by
YELLOW_3:def 2;
then
A5: x9 = [x9`1,x9`2] by MCART_1:21;
A6: [s,t] >> x9 by A4,WAYBEL_3:7;
then t >> x9`2 by A5,Th19;
then
A7: x`2 in waybelow t;
s >> x9`1 by A5,A6,Th19;
then x`1 in waybelow s;
hence thesis by A5,A7,ZFMISC_1:def 2;
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:21;
hereby
let a be object;
assume a in proj1 waybelow x;
then consider b being object such that
A3: [a,b] in waybelow x by XTUPLE_0:def 12;
reconsider b as Element of T by A1,A3,ZFMISC_1:87;
reconsider a9 = a as Element of S by A1,A3,ZFMISC_1:87;
[a9,b] << x by A3,WAYBEL_3:7;
then a9 << x`1 by A2,Th18;
hence a in waybelow x`1;
end;
let b be object;
assume b in proj2 waybelow x;
then consider a being object such that
A4: [a,b] in waybelow x by XTUPLE_0:def 13;
reconsider a as Element of S by A1,A4,ZFMISC_1:87;
reconsider b9 = b as Element of T by A1,A4,ZFMISC_1:87;
[a,b9] << x by A4,WAYBEL_3:7;
then b9 << x`2 by A2,Th18;
hence thesis;
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:];
A1: Bottom T << x`2 by WAYBEL_3:4;
thus proj1 waybelow x c= waybelow x`1 by Th45;
let a be object;
assume
A2: a in waybelow x`1;
then reconsider a9 = a as Element of S;
a9 << x`1 by A2,WAYBEL_3:7;
then [a9,Bottom T] << [x`1,x`2] by A1,Th19;
then
A3: [a9,Bottom T] in waybelow [x`1,x`2];
the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by
YELLOW_3:def 2;
then x = [x`1,x`2] by MCART_1:21;
hence thesis by A3,XTUPLE_0:def 12;
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:];
A1: Bottom S << x`1 by WAYBEL_3:4;
thus proj2 waybelow x c= waybelow x`2 by Th45;
let a be object;
assume
A2: a in waybelow x`2;
then reconsider a9 = a as Element of T;
a9 << x`2 by A2,WAYBEL_3:7;
then [Bottom S,a9] << [x`1,x`2] by A1,Th19;
then
A3: [Bottom S,a9] in waybelow [x`1,x`2];
the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by
YELLOW_3:def 2;
then x = [x`1,x`2] by MCART_1:21;
hence thesis by A3,XTUPLE_0:def 13;
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;
hereby
let x be object;
assume x in [:wayabove s,wayabove t:];
then consider x1, x2 being object such that
A1: x1 in wayabove s and
A2: x2 in wayabove t and
A3: x = [x1,x2] by ZFMISC_1:def 2;
reconsider x2 as Element of T by A2;
reconsider x1 as Element of S by A1;
s << x1 & t << x2 by A1,A2,WAYBEL_3:8;
then [s,t] << [x1,x2] by Th19;
hence x in wayabove [s,t] by A3;
end;
let x be object;
assume
A4: x in wayabove [s,t];
then reconsider x9 = x as Element of [:S,T:];
the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by
YELLOW_3:def 2;
then
A5: x9 = [x9`1,x9`2] by MCART_1:21;
A6: [s,t] << x9 by A4,WAYBEL_3:8;
then t << x9`2 by A5,Th19;
then
A7: x`2 in wayabove t;
s << x9`1 by A5,A6,Th19;
then x`1 in wayabove s;
hence thesis by A5,A7,ZFMISC_1:def 2;
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:21;
hereby
let a be object;
assume a in proj1 wayabove x;
then consider b being object such that
A3: [a,b] in wayabove x by XTUPLE_0:def 12;
reconsider b as Element of T by A1,A3,ZFMISC_1:87;
reconsider a9 = a as Element of S by A1,A3,ZFMISC_1:87;
[a9,b] >> x by A3,WAYBEL_3:8;
then a9 >> x`1 by A2,Th18;
hence a in wayabove x`1;
end;
let b be object;
assume b in proj2 wayabove x;
then consider a being object such that
A4: [a,b] in wayabove x by XTUPLE_0:def 13;
reconsider a as Element of S by A1,A4,ZFMISC_1:87;
reconsider b9 = b as Element of T by A1,A4,ZFMISC_1:87;
[a,b9] >> x by A4,WAYBEL_3:8;
then b9 >> x`2 by A2,Th18;
hence thesis;
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;
hereby
let x be object;
assume x in [:compactbelow s,compactbelow t:];
then consider x1, x2 being object such that
A1: x1 in compactbelow s and
A2: x2 in compactbelow t and
A3: x = [x1,x2] by ZFMISC_1:def 2;
reconsider x2 as Element of T by A2;
reconsider x1 as Element of S by A1;
s >= x1 & t >= x2 by A1,A2,WAYBEL_8:4;
then
A4: [s,t] >= [x1,x2] by YELLOW_3:11;
A5: [x1,x2]`1 = x1 & [x1,x2]`2 = x2;
x1 is compact & x2 is compact by A1,A2,WAYBEL_8:4;
then [x1,x2] is compact by A5,Th23;
hence x in compactbelow [s,t] by A3,A4;
end;
let x be object;
assume
A6: x in compactbelow [s,t];
then reconsider x9 = x as Element of [:S,T:];
A7: x9 is compact by A6,WAYBEL_8:4;
then
A8: x9`1 is compact by Th22;
A9: x9`2 is compact by A7,Th22;
the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by
YELLOW_3:def 2;
then
A10: x9 = [x9`1,x9`2] by MCART_1:21;
A11: [s,t] >= x9 by A6,WAYBEL_8:4;
then t >= x9`2 by A10,YELLOW_3:11;
then
A12: x`2 in compactbelow t by A9;
s >= x9`1 by A10,A11,YELLOW_3:11;
then x`1 in compactbelow s by A8;
hence thesis by A10,A12,ZFMISC_1:def 2;
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:21;
hereby
let a be object;
assume a in proj1 compactbelow x;
then consider b being object such that
A3: [a,b] in compactbelow x by XTUPLE_0:def 12;
reconsider b as Element of T by A1,A3,ZFMISC_1:87;
reconsider a9 = a as Element of S by A1,A3,ZFMISC_1:87;
[a9,b]`1 = a9 & [a9,b] is compact by A3,WAYBEL_8:4;
then
A4: a9 is compact by Th22;
[a9,b] <= x by A3,WAYBEL_8:4;
then a9 <= x`1 by A2,YELLOW_3:11;
hence a in compactbelow x`1 by A4;
end;
let b be object;
assume b in proj2 compactbelow x;
then consider a being object such that
A5: [a,b] in compactbelow x by XTUPLE_0:def 13;
reconsider a as Element of S by A1,A5,ZFMISC_1:87;
reconsider b9 = b as Element of T by A1,A5,ZFMISC_1:87;
[a,b9]`2 = b9 & [a,b9] is compact by A5,WAYBEL_8:4;
then
A6: b9 is compact by Th22;
[a,b9] <= x by A5,WAYBEL_8:4;
then b9 <= x`2 by A2,YELLOW_3:11;
hence thesis by A6;
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:];
A1: Bottom T <= x`2 by YELLOW_0:44;
thus proj1 compactbelow x c= compactbelow x`1 by Th51;
let a be object;
assume
A2: a in compactbelow x`1;
then reconsider a9 = a as Element of S;
a9 <= x`1 by A2,WAYBEL_8:4;
then
A3: [a9,Bottom T] <= [x`1,x`2] by A1,YELLOW_3:11;
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:21;
A5: [a9,Bottom T]`1 = a9 & [a9,Bottom T]`2 = Bottom T;
a9 is compact by A2,WAYBEL_8:4;
then [a9,Bottom T] is compact by A5,Th23,WAYBEL_3:15;
then [a9,Bottom T] in compactbelow [x`1,x`2] by A3;
hence thesis by A4,XTUPLE_0:def 12;
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:];
A1: Bottom S <= x`1 by YELLOW_0:44;
thus proj2 compactbelow x c= compactbelow x`2 by Th51;
let a be object;
assume
A2: a in compactbelow x`2;
then reconsider a9 = a as Element of T;
a9 <= x`2 by A2,WAYBEL_8:4;
then
A3: [Bottom S,a9] <= [x`1,x`2] by A1,YELLOW_3:11;
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:21;
A5: [Bottom S,a9]`1 = Bottom S & [Bottom S,a9]`2 = a9;
a9 is compact by A2,WAYBEL_8:4;
then [Bottom S,a9] is compact by A5,Th23,WAYBEL_3:15;
then [Bottom S,a9] in compactbelow [x`1,x`2] by A3;
hence thesis by A4,XTUPLE_0:def 13;
end;
registration
let S be non empty reflexive RelStr;
cluster empty -> Open for 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 object such that
A3: [s,t] in X by XTUPLE_0:def 12;
reconsider t as Element of T by A2,A3,ZFMISC_1:87;
consider y being Element of [:S,T:] such that
A4: y in X and
A5: y << [s,t] by A1,A3;
take z = y`1;
A6: y = [y`1,y`2] by A2,MCART_1:21;
hence z in proj1 X by A4,XTUPLE_0:def 12;
thus z << s by A5,A6,Th18;
end;
let t be Element of T;
assume t in proj2 X;
then consider s being object such that
A7: [s,t] in X by XTUPLE_0:def 13;
reconsider s as Element of S by A2,A7,ZFMISC_1:87;
consider y being Element of [:S,T:] such that
A8: y in X and
A9: y << [s,t] by A1,A7;
take z = y`2;
A10: y = [y`1,y`2] by A2,MCART_1:21;
hence z in proj2 X by A8,XTUPLE_0:def 13;
thus thesis by A9,A10,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:21;
then x`1 in X by A3,ZFMISC_1:87;
then consider s being Element of S such that
A5: s in X and
A6: s << x`1 by A1;
x`2 in Y by A3,A4,ZFMISC_1:87;
then consider t being Element of T such that
A7: t in Y and
A8: t << x`2 by A2;
reconsider t as Element of T;
take [s,t];
thus [s,t] in [:X,Y:] by A5,A7,ZFMISC_1:87;
thus thesis by A4,A6,A8,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 object such that
A3: [sup D, t] in X by XTUPLE_0:def 12;
A4: t in the carrier of T by A2,A3,ZFMISC_1:87;
then reconsider t9 = {t} as non empty directed Subset of T by WAYBEL_0:5;
ex_sup_of [:D,t9:],[:S,T:] by WAYBEL_0:75;
then sup [:D,t9:] = [sup proj1 [:D,t9:], sup proj2 [:D,t9:]] by YELLOW_3:46
.= [sup D, sup proj2 [:D,t9:]] by FUNCT_5:9
.= [sup D,sup t9] by FUNCT_5:9
.= [sup D,t] by A4,YELLOW_0:39;
then [:D,{t}:] meets X by A1,A3;
then consider x being object such that
A5: x in [:D,{t}:] and
A6: x in X by XBOOLE_0:3;
now
take a = x`1;
x = [a,x`2] by A5,MCART_1:21;
hence a in D & a in proj1 X by A5,A6,XTUPLE_0:def 12,ZFMISC_1:87;
end;
hence D meets proj1 X by XBOOLE_0:3;
end;
let D be non empty directed Subset of T;
assume sup D in proj2 X;
then consider s being object such that
A7: [s,sup D] in X by XTUPLE_0:def 13;
A8: s in the carrier of S by A2,A7,ZFMISC_1:87;
then reconsider s9 = {s} as non empty directed Subset of S by WAYBEL_0:5;
ex_sup_of [:s9,D:],[:S,T:] by WAYBEL_0:75;
then sup [:s9,D:] = [sup proj1 [:s9,D:], sup proj2 [:s9,D:]] by YELLOW_3:46
.= [sup s9, sup proj2 [:s9,D:]] by FUNCT_5:9
.= [sup s9,sup D] by FUNCT_5:9
.= [s,sup D] by A8,YELLOW_0:39;
then [:{s},D:] meets X by A1,A7;
then consider x being object such that
A9: x in [:{s},D:] and
A10: x in X by XBOOLE_0:3;
now
take a = x`2;
x = [x`1,a] by A9,MCART_1:21;
hence a in D & a in proj2 X by A9,A10,XTUPLE_0:def 13,ZFMISC_1:87;
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:];
ex_sup_of D,[:S,T:] by WAYBEL_0:75;
then
A4: sup D = [sup proj1 D, sup proj2 D] by YELLOW_3:46;
then proj1 D is non empty directed & sup proj1 D in X by A3,YELLOW_3:21,22
,ZFMISC_1:87;
then proj1 D meets X by A1;
then consider s being object such that
A5: s in proj1 D and
A6: s in X by XBOOLE_0:3;
reconsider s as Element of S by A5;
consider s2 being object such that
A7: [s,s2] in D by A5,XTUPLE_0:def 12;
proj2 D is non empty directed & sup proj2 D in Y by A3,A4,YELLOW_3:21,22
,ZFMISC_1:87;
then proj2 D meets Y by A2;
then consider t being object such that
A8: t in proj2 D and
A9: t in Y by XBOOLE_0:3;
reconsider t as Element of T by A8;
consider t1 being object such that
A10: [t1,t] in D by A8,XTUPLE_0:def 13;
A11: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by
YELLOW_3:def 2;
then reconsider s2 as Element of T by A7,ZFMISC_1:87;
reconsider t1 as Element of S by A11,A10,ZFMISC_1:87;
consider z being Element of [:S,T:] such that
A12: z in D and
A13: [s,s2] <= z and
A14: [t1,t] <= z by A7,A10,WAYBEL_0:def 1;
now
take z;
thus z in D by A12;
A15: z = [z`1,z`2] by A11,MCART_1:21;
then t <= z`2 by A14,YELLOW_3:11;
then
A16: z`2 in Y by A9,WAYBEL_0:def 20;
s <= z`1 by A13,A15,YELLOW_3:11;
then z`1 in X by A6,WAYBEL_0:def 20;
hence z in [:X,Y:] by A15,A16,ZFMISC_1:87;
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
consider t being object such that
A3: t in Y by A2,XBOOLE_0:def 1;
reconsider t9 = {t} as non empty directed Subset of T by A3,WAYBEL_0:5;
A4: t9 c= Y by A3,ZFMISC_1:31;
let D be non empty directed Subset of S;
assume D c= X;
then
A5: sup [:D,t9:] in [:X,Y:] by A1,A4,ZFMISC_1:96;
ex_sup_of [:D,t9:],[:S,T:] by WAYBEL_0:75;
then sup [:D,t9:] = [sup proj1 [:D,t9:], sup proj2 [:D,t9:]] by
YELLOW_3:46
.= [sup D, sup proj2 [:D,t9:]] by FUNCT_5:9
.= [sup D,sup t9] by FUNCT_5:9
.= [sup D,t] by A3,YELLOW_0:39;
hence thesis by A5,ZFMISC_1:87;
end;
end;
assume X <> {};
then consider s being object such that
A6: s in X by XBOOLE_0:def 1;
reconsider s9 = {s} as non empty directed Subset of S by A6,WAYBEL_0:5;
let D be non empty directed Subset of T such that
A7: D c= Y;
ex_sup_of [:s9,D:],[:S,T:] by WAYBEL_0:75;
then
A8: sup [:s9,D:] = [sup proj1 [:s9,D:], sup proj2 [:s9,D:]] by YELLOW_3:46
.= [sup s9,sup proj2 [:s9,D:]] by FUNCT_5:9
.= [sup s9,sup D] by FUNCT_5:9
.= [s,sup D] by A6,YELLOW_0:39;
s9 c= X by A6,ZFMISC_1:31;
then sup [:s9,D:] in [:X,Y:] by A1,A7,ZFMISC_1:96;
hence thesis by A8,ZFMISC_1:87;
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
A3: D c= [:X,Y:];
proj2 D is non empty directed by YELLOW_3:21,22;
then
A4: sup proj2 D in Y by A2,A3,FUNCT_5:11;
ex_sup_of D,[:S,T:] by WAYBEL_0:75;
then
A5: sup D = [sup proj1 D,sup proj2 D] by YELLOW_3:46;
proj1 D is non empty directed by YELLOW_3:21,22;
then sup proj1 D in X by A1,A3,FUNCT_5:11;
hence thesis by A4,A5,ZFMISC_1:87;
end;
theorem
for S, T being antisymmetric up-complete non empty reflexive RelStr,
X being Subset of [:S,T:] st X is property(S) holds proj1 X is property(S) &
proj2 X is 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 object such that
A3: [sup D, t] in X by XTUPLE_0:def 12;
reconsider t as Element of T by A2,A3,ZFMISC_1:87;
reconsider t9 = {t} as non empty directed Subset of T by WAYBEL_0:5;
ex_sup_of [:D,t9:],[:S,T:] by WAYBEL_0:75;
then sup [:D,t9:] = [sup proj1 [:D,t9:], sup proj2 [:D,t9:]] by YELLOW_3:46
.= [sup D, sup proj2 [:D,t9:]] by FUNCT_5:9
.= [sup D,sup t9] by FUNCT_5:9
.= [sup D,t] by YELLOW_0:39;
then consider y being Element of [:S,T:] such that
A4: y in [:D,t9:] and
A5: for x being Element of [:S,T:] st x in [:D,t9:] & x >= y holds x
in X by A1,A3;
take z = y`1;
A6: y = [y`1,y`2] by A2,MCART_1:21;
hence z in D by A4,ZFMISC_1:87;
A7: y`2 = t by A4,A6,ZFMISC_1:106;
let x be Element of S;
assume x in D;
then
A8: [x,t] in [:D,t9:] by ZFMISC_1:106;
A9: y`2 <= y`2;
assume x >= z;
then [x,t] >= y by A6,A7,A9,YELLOW_3:11;
then [x,t] in X by A5,A8;
hence x in proj1 X by XTUPLE_0:def 12;
end;
let D be non empty directed Subset of T;
assume sup D in proj2 X;
then consider s being object such that
A10: [s,sup D] in X by XTUPLE_0:def 13;
reconsider s as Element of S by A2,A10,ZFMISC_1:87;
reconsider s9 = {s} as non empty directed Subset of S by WAYBEL_0:5;
ex_sup_of [:s9,D:],[:S,T:] by WAYBEL_0:75;
then sup [:s9,D:] = [sup proj1 [:s9,D:], sup proj2 [:s9,D:]] by YELLOW_3:46
.= [sup s9, sup proj2 [:s9,D:]] by FUNCT_5:9
.= [sup s9,sup D] by FUNCT_5:9
.= [s,sup D] by YELLOW_0:39;
then consider y being Element of [:S,T:] such that
A11: y in [:s9,D:] and
A12: for x being Element of [:S,T:] st x in [:s9,D:] & x >= y holds x in
X by A1,A10;
take z = y`2;
A13: y = [y`1,y`2] by A2,MCART_1:21;
hence z in D by A11,ZFMISC_1:87;
A14: y`1 = s by A11,A13,ZFMISC_1:105;
let x be Element of T;
assume x in D;
then
A15: [s,x] in [:s9,D:] by ZFMISC_1:105;
A16: y`1 <= y`1;
assume x >= z;
then [s,x] >= y by A13,A14,A16,YELLOW_3:11;
then [s,x] in X by A12,A15;
hence thesis by XTUPLE_0:def 13;
end;
theorem
for S, T being up-complete non empty Poset, X being Subset of S, Y
being Subset of T st X is property(S) & Y is property(S) holds [:X,Y:] is
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:];
ex_sup_of D,[:S,T:] by WAYBEL_0:75;
then
A4: sup D = [sup proj1 D,sup proj2 D] by YELLOW_3:46;
then proj1 D is non empty directed & sup proj1 D in X by A3,YELLOW_3:21,22
,ZFMISC_1:87;
then consider s being Element of S such that
A5: s in proj1 D and
A6: for x being Element of S st x in proj1 D & x >= s holds x in X by A1;
consider s2 being object such that
A7: [s,s2] in D by A5,XTUPLE_0:def 12;
proj2 D is non empty directed & sup proj2 D in Y by A3,A4,YELLOW_3:21,22
,ZFMISC_1:87;
then 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;
consider t1 being object such that
A10: [t1,t] in D by A8,XTUPLE_0:def 13;
A11: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by
YELLOW_3:def 2;
then reconsider s2 as Element of T by A7,ZFMISC_1:87;
reconsider t1 as Element of S by A11,A10,ZFMISC_1:87;
consider z being Element of [:S,T:] such that
A12: z in D and
A13: [s,s2] <= z and
A14: [t1,t] <= z by A7,A10,WAYBEL_0:def 1;
A15: z = [z`1,z`2] by A11,MCART_1:21;
then
A16: t <= z`2 by A14,YELLOW_3:11;
take z;
thus z in D by A12;
let x be Element of [:S,T:] such that
A17: x in D;
assume
A18: x >= z;
then
A19: x`2 >= z`2 by YELLOW_3:12;
A20: x = [x`1,x`2] by A11,MCART_1:21;
then x`2 in proj2 D by A17,XTUPLE_0:def 13;
then
A21: x`2 in Y by A9,A19,A16,ORDERS_2:3;
A22: s <= z`1 by A13,A15,YELLOW_3:11;
A23: x`1 >= z`1 by A18,YELLOW_3:12;
x`1 in proj1 D by A17,A20,XTUPLE_0:def 12;
then x`1 in X by A6,A23,A22,ORDERS_2:3;
hence thesis by A20,A21,ZFMISC_1:87;
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;
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 A1,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 x >= s by A1,A4,YELLOW_0:2;
hence thesis by A1,YELLOW_0:1;
end;
registration
let S be /\-complete non empty reflexive RelStr;
cluster the RelStr of S -> /\-complete;
coherence by Th62;
end;
registration
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:21;
assume
A6: y is_<=_than X;
then y`2 is_<=_than proj2 X by A5,YELLOW_3:34;
then
A7: t >= y`2 by A4;
y`1 is_<=_than proj1 X by A5,A6,YELLOW_3:34;
then s >= y`1 by A2;
hence thesis by A5,A7,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
set t = the Element of T;
let X be non empty Subset of S;
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:21;
hence x`1 is_<=_than X by A3,YELLOW_3:32;
t <= t;
then
A6: t is_<=_than {t} by YELLOW_0:7;
let y be Element of S;
assume y is_<=_than X;
then x >= [y,t] by A4,A6,YELLOW_3:33;
hence thesis by A5,YELLOW_3:11;
end;
set s = the Element of S;
let X be non empty Subset of T;
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:21;
hence x`2 is_<=_than X by A7,YELLOW_3:32;
s <= s;
then
A10: s is_<=_than {s} by YELLOW_0:7;
let y be Element of T;
assume y is_<=_than X;
then x >= [s,y] by A8,A10,YELLOW_3:33;
hence thesis by A9,YELLOW_3:11;
end;
registration
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];
[s,t]`1 = s & [s,t]`2 = t;
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;
set s = the Element of S;
assume
A1: for x being Element of [:S,T:] ex y being Element of [:S,T:] st y
is_a_complement_of x;
thus S is complemented
proof
set t = the Element of T;
let s be Element of S;
consider y being Element of [:S,T:] such that
A2: y is_a_complement_of [s,t] by A1;
take y`1;
[s,t]`1 = s;
hence y`1 is_a_complement_of s by A2,Th17;
end;
let t be Element of T;
consider y being Element of [:S,T:] such that
A3: y is_a_complement_of [s,t] by A1;
take y`2;
[s,t]`2 = t;
hence y`2 is_a_complement_of t by A3,Th17;
end;
registration
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))`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;
(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;
hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A1,A2,DOMAIN_1:2;
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);
set t = the Element of T;
let x, y, z be Element of S;
A2: t "/\" t = t by YELLOW_0:25;
t <= t;
then
A3: t "\/" t = t by YELLOW_0:24;
thus x "/\" (y "\/" z) = [x "/\" (y "\/" z),t]`1
.= ([x,t] "/\" [y "\/" z,t])`1 by A2,Th15
.= ([x,t] "/\" ([y,t] "\/" [z,t]))`1 by A3,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 A3,Th16
.= (x "/\" y) "\/" (x "/\" z);
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);
set s = the Element of S;
let x, y, z be Element of T;
A2: s "/\" s = s by YELLOW_0:25;
s <= s;
then
A3: s "\/" s = s by YELLOW_0:24;
thus x "/\" (y "\/" z) = [s,x "/\" (y "\/" z)]`2
.= ([s,x] "/\" [s,y "\/" z])`2 by A2,Th15
.= ([s,x] "/\" ([s,y] "\/" [s,z]))`2 by A3,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 A3,Th16
.= (x "/\" y) "\/" (x "/\" z);
end;
registration
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;
reconsider x9 = {x} as non empty directed Subset of [:S,T:] by WAYBEL_0:5;
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:21;
ex_sup_of x9"/\" D,[:S,T:] by WAYBEL_0:75;
then
A5: sup ({x} "/\" D) = [sup proj1 ({x} "/\" D), sup proj2 ({x} "/\" D) ]
by YELLOW_3:46;
ex_sup_of D,[:S,T:] by WAYBEL_0:75;
then
A6: sup D = [sup proj1 D,sup proj2 D] by YELLOW_3:46;
A7: (x "/\" sup D)`2 = x`2 "/\" (sup D)`2 by Th13
.= x`2 "/\" sup proj2 D by A6
.= sup ({x`2} "/\" proj2 D) by A2,WAYBEL_2:def 6
.= sup (proj2 {x} "/\" proj2 D) by A4,FUNCT_5:12
.= sup (proj2 ({x} "/\" D)) by Th24
.= (sup ({x} "/\" D))`2 by A5;
(x "/\" sup D)`1 = x`1 "/\" (sup D)`1 by Th13
.= x`1 "/\" sup proj1 D by A6
.= sup ({x`1} "/\" proj1 D) by A1,WAYBEL_2:def 6
.= sup (proj1 {x} "/\" proj1 D) by A4,FUNCT_5:12
.= sup (proj1 ({x} "/\" D)) by Th24
.= (sup ({x} "/\" D))`1 by A5;
hence x "/\" sup D = sup ({x} "/\" D) by A3,A7,DOMAIN_1:2;
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;
set t = the Element of T;
let s be Element of S, D be non empty directed Subset of S;
reconsider t9 = {t} as non empty directed Subset of T by WAYBEL_0:5;
reconsider ST = {[s,t]} as non empty directed Subset of [:S,T:] by
WAYBEL_0:5;
ex_sup_of [:D,t9:],[:S,T:] by A1,WAYBEL_0:75;
then
A3: sup [:D,t9:] = [sup proj1 [:D,t9:], sup proj2 [:D,t9:]] by YELLOW_3:46;
ex_sup_of ST "/\" [:D,t9:],[:S,T:] by A1,WAYBEL_0:75;
then
A4: sup ({[s,t]} "/\" [:D,t9:]) = [sup proj1 ({[s,t]} "/\" [:D,t9:]), sup
proj2 ({[s,t]} "/\" [:D,t9:])] by YELLOW_3:46;
thus sup ({s} "/\" D) = sup (proj1 {[s,t]} "/\" D) by FUNCT_5:12
.= sup (proj1 {[s,t]} "/\" proj1 [:D,t9:]) by FUNCT_5:9
.= sup proj1 ({[s,t]} "/\" [:D,t9:]) by Th24
.= (sup ({[s,t]} "/\" [:D,t9:]))`1 by A4
.= ([s,t] "/\" sup [:D,t9:] )`1 by A2
.= [s,t]`1 "/\" (sup [:D,t9:])`1 by Th13
.= s "/\" (sup [:D,t9:])`1
.= s "/\" sup proj1 [:D,t9:] by A3
.= s "/\" sup D by FUNCT_5:9;
end;
thus T is up-complete by A1,WAYBEL_2:11;
set s = the Element of S;
let t be Element of T, D be non empty directed Subset of T;
reconsider s9 = {s} as non empty directed Subset of S by WAYBEL_0:5;
ex_sup_of [:s9,D:],[:S,T:] by A1,WAYBEL_0:75;
then
A5: sup [:s9,D:] = [sup proj1 [:s9,D:], sup proj2 [:s9,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 "/\" [:s9,D:],[:S,T:] by A1,WAYBEL_0:75;
then
A6: sup ({[s,t]} "/\" [:s9,D:]) = [sup proj1 ({[s,t]} "/\" [:s9,D:]), sup
proj2 ({[s,t]} "/\" [:s9,D:])] by YELLOW_3:46;
thus sup ({t} "/\" D) = sup (proj2 {[s,t]} "/\" D) by FUNCT_5:12
.= sup (proj2 {[s,t]} "/\" proj2 [:s9,D:]) by FUNCT_5:9
.= sup proj2 ({[s,t]} "/\" [:s9,D:]) by Th24
.= (sup ({[s,t]} "/\" [:s9,D:]))`2 by A6
.= ([s,t] "/\" sup [:s9,D:] )`2 by A2
.= [s,t]`2 "/\" (sup [:s9,D:])`2 by Th13
.= t "/\" (sup [:s9,D:])`2
.= t "/\" sup proj2 [:s9,D:] by A5
.= t "/\" sup D by FUNCT_5:9;
end;
registration
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)`2 = sup proj2 waybelow x
.= sup waybelow x`2 by Th47
.= x`2 by WAYBEL_3:def 5;
(sup waybelow x)`1 = sup proj1 waybelow x by A2
.= sup waybelow x`1 by Th46
.= x`1 by WAYBEL_3:def 5;
hence thesis by A1,A3,DOMAIN_1:2;
end;
end;
registration
let S, T be continuous /\-complete non empty Poset;
cluster [:S,T:] -> continuous;
coherence;
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;
hereby
hereby
set t = the Element of T;
let s be Element of S;
A3: waybelow [s,t] is directed by A1;
[:waybelow s,waybelow t:] = waybelow [s,t] & proj1 [:waybelow s,
waybelow t:] = waybelow s by Th44,FUNCT_5:9;
hence waybelow s is non empty directed by A3,YELLOW_3:22;
end;
thus S is up-complete;
thus S is satisfying_axiom_of_approximation
proof
set t = the Element of T;
let s be Element of S;
waybelow [s,t] is directed by A1;
then ex_sup_of waybelow [s,t], [:S,T:] by WAYBEL_0:75;
then
A4: sup waybelow [s,t] = [sup proj1 waybelow [s,t],sup proj2 waybelow [s
,t]] by Th5;
thus s = [s,t]`1
.= (sup waybelow [s,t])`1 by A2
.= sup proj1 waybelow [s,t] by A4
.= sup waybelow [s,t]`1 by Th46
.= sup waybelow s;
end;
end;
hereby
set s = the Element of S;
let t be Element of T;
A5: waybelow [s,t] is directed by A1;
[:waybelow s,waybelow t:] = waybelow [s,t] & proj2 [:waybelow s,
waybelow t:] = waybelow t by Th44,FUNCT_5:9;
hence waybelow t is non empty directed by A5,YELLOW_3:22;
end;
set s = the Element of S;
thus T is up-complete;
let t be Element of T;
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;
then
A6: sup waybelow [s,t] = [sup proj1 waybelow [s,t],sup proj2 waybelow [s,t
]] by Th5;
thus t = [s,t]`2
.= (sup waybelow [s,t])`2 by A2
.= sup proj2 waybelow [s,t] by A6
.= sup waybelow [s,t]`2 by Th47
.= sup waybelow t;
end;
registration
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)`2 = sup proj2 compactbelow x
.= sup compactbelow x`2 by Th53
.= x`2 by WAYBEL_8:def 3;
(sup compactbelow x)`1 = sup proj1 compactbelow x by A2
.= sup compactbelow x`1 by Th52
.= x`1 by WAYBEL_8:def 3;
hence thesis by A1,A3,DOMAIN_1:2;
end;
end;
registration
let S, T be complete algebraic lower-bounded sup-Semilattice;
cluster [:S,T:] -> algebraic;
coherence;
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
set t = the Element of T;
let s be Element of S;
A4: compactbelow [s,t] is directed by A1;
[:compactbelow s,compactbelow t:] = compactbelow [s,t] & proj1 [:
compactbelow s,compactbelow t:] = compactbelow s by A3,Th50,FUNCT_5:9;
hence compactbelow s is non empty directed by A4,YELLOW_3:22;
end;
thus S is up-complete by A2,WAYBEL_2:11;
thus S is satisfying_axiom_K
proof
set t = the Element of T;
let s be 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
A5: sup compactbelow [s,t] = [sup proj1 compactbelow [s,t],sup proj2
compactbelow [s,t]] by Th5;
thus s = [s,t]`1
.= (sup compactbelow [s,t])`1 by A2
.= sup proj1 compactbelow [s,t] by A5
.= sup compactbelow [s,t]`1 by A3,Th52
.= sup compactbelow s;
end;
end;
set s = the Element of S;
hereby
set s = the Element of S;
let t be Element of T;
A6: compactbelow [s,t] is directed by A1;
[:compactbelow s,compactbelow t:] = compactbelow [s,t] & proj2 [:
compactbelow s,compactbelow t:] = compactbelow t by A3,Th50,FUNCT_5:9;
hence compactbelow t is non empty directed by A6,YELLOW_3:22;
end;
thus T is up-complete by A2,WAYBEL_2:11;
let t be 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
A7: sup compactbelow [s,t] = [sup proj1 compactbelow [s,t],sup proj2
compactbelow [s,t]] by Th5;
thus t = [s,t]`2
.= (sup compactbelow [s,t])`2 by A2
.= sup proj2 compactbelow [s,t] by A7
.= sup compactbelow [s,t]`2 by A3,Th53
.= sup compactbelow t;
end;
registration
let S, T be arithmetic lower-bounded LATTICE;
cluster [:S,T:] -> arithmetic;
coherence
proof
set C = CompactSublatt [:S,T:];
thus [:S,T:] is algebraic;
let x, y be Element of [:S,T:] such that
A1: x in the carrier of C and
A2: y in the carrier of C and
ex_inf_of {x,y},[:S,T:];
A3: x is compact by A1,WAYBEL_8:def 1;
then x`1 is compact by Th22;
then
A4: x`1 in the carrier of CompactSublatt S by WAYBEL_8:def 1;
A5: y is compact by A2,WAYBEL_8:def 1;
then y`1 is compact by Th22;
then
A6: y`1 in the carrier of CompactSublatt S by WAYBEL_8:def 1;
x`2 is compact by A3,Th22;
then
A7: x`2 in the carrier of CompactSublatt T by WAYBEL_8:def 1;
y`2 is compact by A5,Th22;
then
A8: y`2 in the carrier of CompactSublatt T by WAYBEL_8:def 1;
CompactSublatt T is meet-inheriting & ex_inf_of {x`2,y`2},T by
WAYBEL_8:def 5,YELLOW_0:21;
then inf {x`2,y`2} in the carrier of CompactSublatt T by A7,A8;
then x`2 "/\" y`2 in the carrier of CompactSublatt T by YELLOW_0:40;
then x`2 "/\" y`2 is compact by WAYBEL_8:def 1;
then
A9: (x "/\" y)`2 is compact by Th13;
CompactSublatt S is meet-inheriting & ex_inf_of {x`1,y`1},S by
WAYBEL_8:def 5,YELLOW_0:21;
then inf {x`1,y`1} in the carrier of CompactSublatt S by A4,A6;
then x`1 "/\" y`1 in the carrier of CompactSublatt S by YELLOW_0:40;
then x`1 "/\" y`1 is compact by WAYBEL_8:def 1;
then (x "/\" y)`1 is compact by Th13;
then x "/\" y is compact by A9,Th23;
then inf {x,y} is compact by YELLOW_0:40;
hence thesis 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;
A3: S is up-complete & T is up-complete by A1,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 and
A5: y in the carrier of CompactSublatt S and
ex_inf_of {x,y},S;
A6: [y,Bottom T]`1 = y & [y, Bottom T]`2 = Bottom T;
y is compact by A5,WAYBEL_8:def 1;
then [y,Bottom T] is compact by A3,A6,Th23,WAYBEL_3:15;
then
A7: [y,Bottom T] in the carrier of CompactSublatt [:S,T:] by WAYBEL_8:def 1;
A8: [x,Bottom T]`1 = x & [x,Bottom T]`2 = Bottom T;
x is compact by A4,WAYBEL_8:def 1;
then [x,Bottom T] is compact by A3,A8,Th23,WAYBEL_3:15;
then
ex_inf_of {[x,Bottom T], [y,Bottom T]}, [:S,T:] & [x,Bottom T] in the
carrier of CompactSublatt [:S,T:] by WAYBEL_8:def 1,YELLOW_0:21;
then
inf {[x,Bottom T], [y,Bottom T]} in the carrier of CompactSublatt [:S
,T:] by A2,A7;
then
A9: 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
.= x "/\" y;
then x "/\" y is compact by A3,A9,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
A10: x in the carrier of CompactSublatt T and
A11: y in the carrier of CompactSublatt T and
ex_inf_of {x,y},T;
A12: [Bottom S,y]`2 = y & [ Bottom S,y]`1 = Bottom S;
y is compact by A11,WAYBEL_8:def 1;
then [Bottom S,y] is compact by A3,A12,Th23,WAYBEL_3:15;
then
A13: [Bottom S,y] in the carrier of CompactSublatt [:S,T:] by WAYBEL_8:def 1;
A14: [Bottom S,x]`2 = x & [Bottom S,x]`1 = Bottom S;
x is compact by A10,WAYBEL_8:def 1;
then [Bottom S,x] is compact by A3,A14,Th23,WAYBEL_3:15;
then ex_inf_of {[Bottom S,x], [Bottom S,y]}, [:S,T:] & [Bottom S,x] in the
carrier of CompactSublatt [:S,T:] by WAYBEL_8:def 1,YELLOW_0:21;
then
inf {[Bottom S,x], [Bottom S,y]} in the carrier of CompactSublatt [:S,
T:] by A2,A13;
then
A15: 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
.= x "/\" y;
then x "/\" y is compact by A3,A15,Th22;
then inf {x,y} is compact by YELLOW_0:40;
hence thesis by WAYBEL_8:def 1;
end;