:: by Artur Korni{\l}owicz

::

:: Received September 25, 1996

:: Copyright (c) 1996-2012 Association of Mizar Users

begin

registration

let L be RelStr ;

let X be empty Subset of L;

coherence

downarrow X is empty

uparrow X is empty

end;
let X be empty Subset of L;

coherence

downarrow X is empty

proof end;

coherence uparrow X is empty

proof end;

Lm1: for x, a1, a2, b1, b2 being set st x = [[a1,a2],[b1,b2]] holds

( (x `1) `1 = a1 & (x `1) `2 = a2 & (x `2) `1 = b1 & (x `2) `2 = b2 )

proof end;

theorem :: YELLOW_3:2

for L being transitive antisymmetric with_infima RelStr

for a, b, c, d being Element of L st a <= c & b <= d holds

a "/\" b <= c "/\" d

for a, b, c, d being Element of L st a <= c & b <= d holds

a "/\" b <= c "/\" d

proof end;

theorem :: YELLOW_3:3

for L being transitive antisymmetric with_suprema RelStr

for a, b, c, d being Element of L st a <= c & b <= d holds

a "\/" b <= c "\/" d

for a, b, c, d being Element of L st a <= c & b <= d holds

a "\/" b <= c "\/" d

proof end;

theorem :: YELLOW_3:4

for L being non empty reflexive antisymmetric complete RelStr

for D being Subset of L

for x being Element of L st x in D holds

(sup D) "/\" x = x

for D being Subset of L

for x being Element of L st x in D holds

(sup D) "/\" x = x

proof end;

theorem :: YELLOW_3:5

for L being non empty reflexive antisymmetric complete RelStr

for D being Subset of L

for x being Element of L st x in D holds

(inf D) "\/" x = x

for D being Subset of L

for x being Element of L st x in D holds

(inf D) "\/" x = x

proof end;

theorem :: YELLOW_3:8

for S, T being with_infima Poset

for f being Function of S,T

for x, y being Element of S holds

( f preserves_inf_of {x,y} iff f . (x "/\" y) = (f . x) "/\" (f . y) )

for f being Function of S,T

for x, y being Element of S holds

( f preserves_inf_of {x,y} iff f . (x "/\" y) = (f . x) "/\" (f . y) )

proof end;

theorem :: YELLOW_3:9

for S, T being with_suprema Poset

for f being Function of S,T

for x, y being Element of S holds

( f preserves_sup_of {x,y} iff f . (x "\/" y) = (f . x) "\/" (f . y) )

for f being Function of S,T

for x, y being Element of S holds

( f preserves_sup_of {x,y} iff f . (x "\/" y) = (f . x) "\/" (f . y) )

proof end;

begin

definition

let P, R be Relation;

ex b_{1} being Relation st

for x, y being set holds

( [x,y] in b_{1} iff ex p, q, s, t being set st

( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) )

for b_{1}, b_{2} being Relation st ( for x, y being set holds

( [x,y] in b_{1} iff ex p, q, s, t being set st

( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ) ) & ( for x, y being set holds

( [x,y] in b_{2} iff ex p, q, s, t being set st

( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ) ) holds

b_{1} = b_{2}

end;
func ["P,R"] -> Relation means :Def1: :: YELLOW_3:def 1

for x, y being set holds

( [x,y] in it iff ex p, q, s, t being set st

( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) );

existence for x, y being set holds

( [x,y] in it iff ex p, q, s, t being set st

( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) );

ex b

for x, y being set holds

( [x,y] in b

( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) )

proof end;

uniqueness for b

( [x,y] in b

( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ) ) & ( for x, y being set holds

( [x,y] in b

( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ) ) holds

b

proof end;

:: deftheorem Def1 defines [" YELLOW_3:def 1 :

for P, R, b_{3} being Relation holds

( b_{3} = ["P,R"] iff for x, y being set holds

( [x,y] in b_{3} iff ex p, q, s, t being set st

( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ) );

for P, R, b

( b

( [x,y] in b

( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ) );

theorem Th10: :: YELLOW_3:10

for P, R being Relation

for x being set holds

( x in ["P,R"] iff ( [((x `1) `1),((x `2) `1)] in P & [((x `1) `2),((x `2) `2)] in R & ex a, b being set st x = [a,b] & ex c, d being set st x `1 = [c,d] & ex e, f being set st x `2 = [e,f] ) )

for x being set holds

( x in ["P,R"] iff ( [((x `1) `1),((x `2) `1)] in P & [((x `1) `2),((x `2) `2)] in R & ex a, b being set st x = [a,b] & ex c, d being set st x `1 = [c,d] & ex e, f being set st x `2 = [e,f] ) )

proof end;

definition

let A, B, X, Y be set ;

let P be Relation of A,B;

let R be Relation of X,Y;

:: original: ["

redefine func ["P,R"] -> Relation of [:A,X:],[:B,Y:];

coherence

["P,R"] is Relation of [:A,X:],[:B,Y:]

end;
let P be Relation of A,B;

let R be Relation of X,Y;

:: original: ["

redefine func ["P,R"] -> Relation of [:A,X:],[:B,Y:];

coherence

["P,R"] is Relation of [:A,X:],[:B,Y:]

proof end;

definition

let X, Y be RelStr ;

ex b_{1} being strict RelStr st

( the carrier of b_{1} = [: the carrier of X, the carrier of Y:] & the InternalRel of b_{1} = [" the InternalRel of X, the InternalRel of Y"] )

for b_{1}, b_{2} being strict RelStr st the carrier of b_{1} = [: the carrier of X, the carrier of Y:] & the InternalRel of b_{1} = [" the InternalRel of X, the InternalRel of Y"] & the carrier of b_{2} = [: the carrier of X, the carrier of Y:] & the InternalRel of b_{2} = [" the InternalRel of X, the InternalRel of Y"] holds

b_{1} = b_{2}
;

end;
func [:X,Y:] -> strict RelStr means :Def2: :: YELLOW_3:def 2

( the carrier of it = [: the carrier of X, the carrier of Y:] & the InternalRel of it = [" the InternalRel of X, the InternalRel of Y"] );

existence ( the carrier of it = [: the carrier of X, the carrier of Y:] & the InternalRel of it = [" the InternalRel of X, the InternalRel of Y"] );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def2 defines [: YELLOW_3:def 2 :

for X, Y being RelStr

for b_{3} being strict RelStr holds

( b_{3} = [:X,Y:] iff ( the carrier of b_{3} = [: the carrier of X, the carrier of Y:] & the InternalRel of b_{3} = [" the InternalRel of X, the InternalRel of Y"] ) );

for X, Y being RelStr

for b

( b

definition

let L1, L2 be RelStr ;

let D be Subset of [:L1,L2:];

:: original: proj1

redefine func proj1 D -> Subset of L1;

coherence

proj1 D is Subset of L1

redefine func proj2 D -> Subset of L2;

coherence

proj2 D is Subset of L2

end;
let D be Subset of [:L1,L2:];

:: original: proj1

redefine func proj1 D -> Subset of L1;

coherence

proj1 D is Subset of L1

proof end;

:: original: proj2redefine func proj2 D -> Subset of L2;

coherence

proj2 D is Subset of L2

proof end;

definition

let S1, S2 be RelStr ;

let D1 be Subset of S1;

let D2 be Subset of S2;

:: original: [:

redefine func [:D1,D2:] -> Subset of [:S1,S2:];

coherence

[:D1,D2:] is Subset of [:S1,S2:]

end;
let D1 be Subset of S1;

let D2 be Subset of S2;

:: original: [:

redefine func [:D1,D2:] -> Subset of [:S1,S2:];

coherence

[:D1,D2:] is Subset of [:S1,S2:]

proof end;

definition

let S1, S2 be non empty RelStr ;

let x be Element of S1;

let y be Element of S2;

:: original: [

redefine func [x,y] -> Element of [:S1,S2:];

coherence

[x,y] is Element of [:S1,S2:]

end;
let x be Element of S1;

let y be Element of S2;

:: original: [

redefine func [x,y] -> Element of [:S1,S2:];

coherence

[x,y] is Element of [:S1,S2:]

proof end;

definition

let L1, L2 be non empty RelStr ;

let x be Element of [:L1,L2:];

:: original: `1

redefine func x `1 -> Element of L1;

coherence

x `1 is Element of L1

redefine func x `2 -> Element of L2;

coherence

x `2 is Element of L2

end;
let x be Element of [:L1,L2:];

:: original: `1

redefine func x `1 -> Element of L1;

coherence

x `1 is Element of L1

proof end;

:: original: `2redefine func x `2 -> Element of L2;

coherence

x `2 is Element of L2

proof end;

theorem Th11: :: YELLOW_3:11

for S1, S2 being non empty RelStr

for a, c being Element of S1

for b, d being Element of S2 holds

( ( a <= c & b <= d ) iff [a,b] <= [c,d] )

for a, c being Element of S1

for b, d being Element of S2 holds

( ( a <= c & b <= d ) iff [a,b] <= [c,d] )

proof end;

theorem Th12: :: YELLOW_3:12

for S1, S2 being non empty RelStr

for x, y being Element of [:S1,S2:] holds

( x <= y iff ( x `1 <= y `1 & x `2 <= y `2 ) )

for x, y being Element of [:S1,S2:] holds

( x <= y iff ( x `1 <= y `1 & x `2 <= y `2 ) )

proof end;

theorem :: YELLOW_3:13

for A, B being RelStr

for C being non empty RelStr

for f, g being Function of [:A,B:],C st ( for x being Element of A

for y being Element of B holds f . (x,y) = g . (x,y) ) holds

f = g

for C being non empty RelStr

for f, g being Function of [:A,B:],C st ( for x being Element of A

for y being Element of B holds f . (x,y) = g . (x,y) ) holds

f = g

proof end;

theorem :: YELLOW_3:16

for X, Y being non empty reflexive RelStr st [:X,Y:] is antisymmetric holds

( X is antisymmetric & Y is antisymmetric )

( X is antisymmetric & Y is antisymmetric )

proof end;

theorem :: YELLOW_3:17

for X, Y being non empty reflexive RelStr st [:X,Y:] is transitive holds

( X is transitive & Y is transitive )

( X is transitive & Y is transitive )

proof end;

theorem :: YELLOW_3:18

for X, Y being non empty reflexive RelStr st [:X,Y:] is with_suprema holds

( X is with_suprema & Y is with_suprema )

( X is with_suprema & Y is with_suprema )

proof end;

theorem :: YELLOW_3:19

for X, Y being non empty reflexive RelStr st [:X,Y:] is with_infima holds

( X is with_infima & Y is with_infima )

( X is with_infima & Y is with_infima )

proof end;

definition

let S1, S2 be RelStr ;

let D1 be directed Subset of S1;

let D2 be directed Subset of S2;

:: original: [:

redefine func [:D1,D2:] -> directed Subset of [:S1,S2:];

coherence

[:D1,D2:] is directed Subset of [:S1,S2:]

end;
let D1 be directed Subset of S1;

let D2 be directed Subset of S2;

:: original: [:

redefine func [:D1,D2:] -> directed Subset of [:S1,S2:];

coherence

[:D1,D2:] is directed Subset of [:S1,S2:]

proof end;

theorem :: YELLOW_3:20

for S1, S2 being non empty RelStr

for D1 being non empty Subset of S1

for D2 being non empty Subset of S2 st [:D1,D2:] is directed holds

( D1 is directed & D2 is directed )

for D1 being non empty Subset of S1

for D2 being non empty Subset of S2 st [:D1,D2:] is directed holds

( D1 is directed & D2 is directed )

proof end;

theorem Th21: :: YELLOW_3:21

for S1, S2 being non empty RelStr

for D being non empty Subset of [:S1,S2:] holds

( not proj1 D is empty & not proj2 D is empty )

for D being non empty Subset of [:S1,S2:] holds

( not proj1 D is empty & not proj2 D is empty )

proof end;

theorem :: YELLOW_3:22

for S1, S2 being non empty reflexive RelStr

for D being non empty directed Subset of [:S1,S2:] holds

( proj1 D is directed & proj2 D is directed )

for D being non empty directed Subset of [:S1,S2:] holds

( proj1 D is directed & proj2 D is directed )

proof end;

definition

let S1, S2 be RelStr ;

let D1 be filtered Subset of S1;

let D2 be filtered Subset of S2;

:: original: [:

redefine func [:D1,D2:] -> filtered Subset of [:S1,S2:];

coherence

[:D1,D2:] is filtered Subset of [:S1,S2:]

end;
let D1 be filtered Subset of S1;

let D2 be filtered Subset of S2;

:: original: [:

redefine func [:D1,D2:] -> filtered Subset of [:S1,S2:];

coherence

[:D1,D2:] is filtered Subset of [:S1,S2:]

proof end;

theorem :: YELLOW_3:23

for S1, S2 being non empty RelStr

for D1 being non empty Subset of S1

for D2 being non empty Subset of S2 st [:D1,D2:] is filtered holds

( D1 is filtered & D2 is filtered )

for D1 being non empty Subset of S1

for D2 being non empty Subset of S2 st [:D1,D2:] is filtered holds

( D1 is filtered & D2 is filtered )

proof end;

theorem :: YELLOW_3:24

for S1, S2 being non empty reflexive RelStr

for D being non empty filtered Subset of [:S1,S2:] holds

( proj1 D is filtered & proj2 D is filtered )

for D being non empty filtered Subset of [:S1,S2:] holds

( proj1 D is filtered & proj2 D is filtered )

proof end;

definition

let S1, S2 be RelStr ;

let D1 be upper Subset of S1;

let D2 be upper Subset of S2;

:: original: [:

redefine func [:D1,D2:] -> upper Subset of [:S1,S2:];

coherence

[:D1,D2:] is upper Subset of [:S1,S2:]

end;
let D1 be upper Subset of S1;

let D2 be upper Subset of S2;

:: original: [:

redefine func [:D1,D2:] -> upper Subset of [:S1,S2:];

coherence

[:D1,D2:] is upper Subset of [:S1,S2:]

proof end;

theorem :: YELLOW_3:25

for S1, S2 being non empty reflexive RelStr

for D1 being non empty Subset of S1

for D2 being non empty Subset of S2 st [:D1,D2:] is upper holds

( D1 is upper & D2 is upper )

for D1 being non empty Subset of S1

for D2 being non empty Subset of S2 st [:D1,D2:] is upper holds

( D1 is upper & D2 is upper )

proof end;

theorem :: YELLOW_3:26

for S1, S2 being non empty reflexive RelStr

for D being non empty upper Subset of [:S1,S2:] holds

( proj1 D is upper & proj2 D is upper )

for D being non empty upper Subset of [:S1,S2:] holds

( proj1 D is upper & proj2 D is upper )

proof end;

definition

let S1, S2 be RelStr ;

let D1 be lower Subset of S1;

let D2 be lower Subset of S2;

:: original: [:

redefine func [:D1,D2:] -> lower Subset of [:S1,S2:];

coherence

[:D1,D2:] is lower Subset of [:S1,S2:]

end;
let D1 be lower Subset of S1;

let D2 be lower Subset of S2;

:: original: [:

redefine func [:D1,D2:] -> lower Subset of [:S1,S2:];

coherence

[:D1,D2:] is lower Subset of [:S1,S2:]

proof end;

theorem :: YELLOW_3:27

for S1, S2 being non empty reflexive RelStr

for D1 being non empty Subset of S1

for D2 being non empty Subset of S2 st [:D1,D2:] is lower holds

( D1 is lower & D2 is lower )

for D1 being non empty Subset of S1

for D2 being non empty Subset of S2 st [:D1,D2:] is lower holds

( D1 is lower & D2 is lower )

proof end;

theorem :: YELLOW_3:28

for S1, S2 being non empty reflexive RelStr

for D being non empty lower Subset of [:S1,S2:] holds

( proj1 D is lower & proj2 D is lower )

for D being non empty lower Subset of [:S1,S2:] holds

( proj1 D is lower & proj2 D is lower )

proof end;

definition
end;

:: deftheorem Def3 defines void YELLOW_3:def 3 :

for R being RelStr holds

( R is void iff the InternalRel of R is empty );

for R being RelStr holds

( R is void iff the InternalRel of R is empty );

registration

existence

ex b_{1} being Poset st

( not b_{1} is void & not b_{1} is empty & b_{1} is strict )

end;
ex b

( not b

proof end;

registration

coherence

for b_{1} being RelStr st not b_{1} is empty & b_{1} is reflexive holds

not b_{1} is void

end;
for b

not b

proof end;

theorem Th29: :: YELLOW_3:29

for S1, S2 being non empty RelStr

for D1 being non empty Subset of S1

for D2 being non empty Subset of S2

for x being Element of S1

for y being Element of S2 st [x,y] is_>=_than [:D1,D2:] holds

( x is_>=_than D1 & y is_>=_than D2 )

for D1 being non empty Subset of S1

for D2 being non empty Subset of S2

for x being Element of S1

for y being Element of S2 st [x,y] is_>=_than [:D1,D2:] holds

( x is_>=_than D1 & y is_>=_than D2 )

proof end;

theorem Th30: :: YELLOW_3:30

for S1, S2 being non empty RelStr

for D1 being Subset of S1

for D2 being Subset of S2

for x being Element of S1

for y being Element of S2 st x is_>=_than D1 & y is_>=_than D2 holds

[x,y] is_>=_than [:D1,D2:]

for D1 being Subset of S1

for D2 being Subset of S2

for x being Element of S1

for y being Element of S2 st x is_>=_than D1 & y is_>=_than D2 holds

[x,y] is_>=_than [:D1,D2:]

proof end;

theorem Th31: :: YELLOW_3:31

for S1, S2 being non empty RelStr

for D being Subset of [:S1,S2:]

for x being Element of S1

for y being Element of S2 holds

( [x,y] is_>=_than D iff ( x is_>=_than proj1 D & y is_>=_than proj2 D ) )

for D being Subset of [:S1,S2:]

for x being Element of S1

for y being Element of S2 holds

( [x,y] is_>=_than D iff ( x is_>=_than proj1 D & y is_>=_than proj2 D ) )

proof end;

theorem Th32: :: YELLOW_3:32

for S1, S2 being non empty RelStr

for D1 being non empty Subset of S1

for D2 being non empty Subset of S2

for x being Element of S1

for y being Element of S2 st [x,y] is_<=_than [:D1,D2:] holds

( x is_<=_than D1 & y is_<=_than D2 )

for D1 being non empty Subset of S1

for D2 being non empty Subset of S2

for x being Element of S1

for y being Element of S2 st [x,y] is_<=_than [:D1,D2:] holds

( x is_<=_than D1 & y is_<=_than D2 )

proof end;

theorem Th33: :: YELLOW_3:33

for S1, S2 being non empty RelStr

for D1 being Subset of S1

for D2 being Subset of S2

for x being Element of S1

for y being Element of S2 st x is_<=_than D1 & y is_<=_than D2 holds

[x,y] is_<=_than [:D1,D2:]

for D1 being Subset of S1

for D2 being Subset of S2

for x being Element of S1

for y being Element of S2 st x is_<=_than D1 & y is_<=_than D2 holds

[x,y] is_<=_than [:D1,D2:]

proof end;

theorem Th34: :: YELLOW_3:34

for S1, S2 being non empty RelStr

for D being Subset of [:S1,S2:]

for x being Element of S1

for y being Element of S2 holds

( [x,y] is_<=_than D iff ( x is_<=_than proj1 D & y is_<=_than proj2 D ) )

for D being Subset of [:S1,S2:]

for x being Element of S1

for y being Element of S2 holds

( [x,y] is_<=_than D iff ( x is_<=_than proj1 D & y is_<=_than proj2 D ) )

proof end;

theorem Th35: :: YELLOW_3:35

for S1, S2 being non empty antisymmetric RelStr

for D1 being Subset of S1

for D2 being Subset of S2

for x being Element of S1

for y being Element of S2 st ex_sup_of D1,S1 & ex_sup_of D2,S2 & ( for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds

[x,y] <= b ) holds

( ( for c being Element of S1 st c is_>=_than D1 holds

x <= c ) & ( for d being Element of S2 st d is_>=_than D2 holds

y <= d ) )

for D1 being Subset of S1

for D2 being Subset of S2

for x being Element of S1

for y being Element of S2 st ex_sup_of D1,S1 & ex_sup_of D2,S2 & ( for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds

[x,y] <= b ) holds

( ( for c being Element of S1 st c is_>=_than D1 holds

x <= c ) & ( for d being Element of S2 st d is_>=_than D2 holds

y <= d ) )

proof end;

theorem Th36: :: YELLOW_3:36

for S1, S2 being non empty antisymmetric RelStr

for D1 being Subset of S1

for D2 being Subset of S2

for x being Element of S1

for y being Element of S2 st ex_inf_of D1,S1 & ex_inf_of D2,S2 & ( for b being Element of [:S1,S2:] st b is_<=_than [:D1,D2:] holds

[x,y] >= b ) holds

( ( for c being Element of S1 st c is_<=_than D1 holds

x >= c ) & ( for d being Element of S2 st d is_<=_than D2 holds

y >= d ) )

for D1 being Subset of S1

for D2 being Subset of S2

for x being Element of S1

for y being Element of S2 st ex_inf_of D1,S1 & ex_inf_of D2,S2 & ( for b being Element of [:S1,S2:] st b is_<=_than [:D1,D2:] holds

[x,y] >= b ) holds

( ( for c being Element of S1 st c is_<=_than D1 holds

x >= c ) & ( for d being Element of S2 st d is_<=_than D2 holds

y >= d ) )

proof end;

theorem :: YELLOW_3:37

for S1, S2 being non empty antisymmetric RelStr

for D1 being non empty Subset of S1

for D2 being non empty Subset of S2

for x being Element of S1

for y being Element of S2 st ( for c being Element of S1 st c is_>=_than D1 holds

x <= c ) & ( for d being Element of S2 st d is_>=_than D2 holds

y <= d ) holds

for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds

[x,y] <= b

for D1 being non empty Subset of S1

for D2 being non empty Subset of S2

for x being Element of S1

for y being Element of S2 st ( for c being Element of S1 st c is_>=_than D1 holds

x <= c ) & ( for d being Element of S2 st d is_>=_than D2 holds

y <= d ) holds

for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds

[x,y] <= b

proof end;

theorem :: YELLOW_3:38

for S1, S2 being non empty antisymmetric RelStr

for D1 being non empty Subset of S1

for D2 being non empty Subset of S2

for x being Element of S1

for y being Element of S2 st ( for c being Element of S1 st c is_>=_than D1 holds

x >= c ) & ( for d being Element of S2 st d is_>=_than D2 holds

y >= d ) holds

for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds

[x,y] >= b

for D1 being non empty Subset of S1

for D2 being non empty Subset of S2

for x being Element of S1

for y being Element of S2 st ( for c being Element of S1 st c is_>=_than D1 holds

x >= c ) & ( for d being Element of S2 st d is_>=_than D2 holds

y >= d ) holds

for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds

[x,y] >= b

proof end;

theorem Th39: :: YELLOW_3:39

for S1, S2 being non empty antisymmetric RelStr

for D1 being non empty Subset of S1

for D2 being non empty Subset of S2 holds

( ( ex_sup_of D1,S1 & ex_sup_of D2,S2 ) iff ex_sup_of [:D1,D2:],[:S1,S2:] )

for D1 being non empty Subset of S1

for D2 being non empty Subset of S2 holds

( ( ex_sup_of D1,S1 & ex_sup_of D2,S2 ) iff ex_sup_of [:D1,D2:],[:S1,S2:] )

proof end;

theorem Th40: :: YELLOW_3:40

for S1, S2 being non empty antisymmetric RelStr

for D1 being non empty Subset of S1

for D2 being non empty Subset of S2 holds

( ( ex_inf_of D1,S1 & ex_inf_of D2,S2 ) iff ex_inf_of [:D1,D2:],[:S1,S2:] )

for D1 being non empty Subset of S1

for D2 being non empty Subset of S2 holds

( ( ex_inf_of D1,S1 & ex_inf_of D2,S2 ) iff ex_inf_of [:D1,D2:],[:S1,S2:] )

proof end;

theorem Th41: :: YELLOW_3:41

for S1, S2 being non empty antisymmetric RelStr

for D being Subset of [:S1,S2:] holds

( ( ex_sup_of proj1 D,S1 & ex_sup_of proj2 D,S2 ) iff ex_sup_of D,[:S1,S2:] )

for D being Subset of [:S1,S2:] holds

( ( ex_sup_of proj1 D,S1 & ex_sup_of proj2 D,S2 ) iff ex_sup_of D,[:S1,S2:] )

proof end;

theorem Th42: :: YELLOW_3:42

for S1, S2 being non empty antisymmetric RelStr

for D being Subset of [:S1,S2:] holds

( ( ex_inf_of proj1 D,S1 & ex_inf_of proj2 D,S2 ) iff ex_inf_of D,[:S1,S2:] )

for D being Subset of [:S1,S2:] holds

( ( ex_inf_of proj1 D,S1 & ex_inf_of proj2 D,S2 ) iff ex_inf_of D,[:S1,S2:] )

proof end;

theorem Th43: :: YELLOW_3:43

for S1, S2 being non empty antisymmetric RelStr

for D1 being non empty Subset of S1

for D2 being non empty Subset of S2 st ex_sup_of D1,S1 & ex_sup_of D2,S2 holds

sup [:D1,D2:] = [(sup D1),(sup D2)]

for D1 being non empty Subset of S1

for D2 being non empty Subset of S2 st ex_sup_of D1,S1 & ex_sup_of D2,S2 holds

sup [:D1,D2:] = [(sup D1),(sup D2)]

proof end;

theorem Th44: :: YELLOW_3:44

for S1, S2 being non empty antisymmetric RelStr

for D1 being non empty Subset of S1

for D2 being non empty Subset of S2 st ex_inf_of D1,S1 & ex_inf_of D2,S2 holds

inf [:D1,D2:] = [(inf D1),(inf D2)]

for D1 being non empty Subset of S1

for D2 being non empty Subset of S2 st ex_inf_of D1,S1 & ex_inf_of D2,S2 holds

inf [:D1,D2:] = [(inf D1),(inf D2)]

proof end;

registration
end;

theorem :: YELLOW_3:45

for X, Y being non empty antisymmetric lower-bounded RelStr st [:X,Y:] is complete holds

( X is complete & Y is complete )

( X is complete & Y is complete )

proof end;

theorem :: YELLOW_3:46

for L1, L2 being non empty antisymmetric RelStr

for D being non empty Subset of [:L1,L2:] st ( [:L1,L2:] is complete or ex_sup_of D,[:L1,L2:] ) holds

sup D = [(sup (proj1 D)),(sup (proj2 D))]

for D being non empty Subset of [:L1,L2:] st ( [:L1,L2:] is complete or ex_sup_of D,[:L1,L2:] ) holds

sup D = [(sup (proj1 D)),(sup (proj2 D))]

proof end;

theorem :: YELLOW_3:47

for L1, L2 being non empty antisymmetric RelStr

for D being non empty Subset of [:L1,L2:] st ( [:L1,L2:] is complete or ex_inf_of D,[:L1,L2:] ) holds

inf D = [(inf (proj1 D)),(inf (proj2 D))]

for D being non empty Subset of [:L1,L2:] st ( [:L1,L2:] is complete or ex_inf_of D,[:L1,L2:] ) holds

inf D = [(inf (proj1 D)),(inf (proj2 D))]

proof end;

theorem :: YELLOW_3:48

for S1, S2 being non empty reflexive RelStr

for D being non empty directed Subset of [:S1,S2:] holds [:(proj1 D),(proj2 D):] c= downarrow D

for D being non empty directed Subset of [:S1,S2:] holds [:(proj1 D),(proj2 D):] c= downarrow D

proof end;

theorem :: YELLOW_3:49

for S1, S2 being non empty reflexive RelStr

for D being non empty filtered Subset of [:S1,S2:] holds [:(proj1 D),(proj2 D):] c= uparrow D

for D being non empty filtered Subset of [:S1,S2:] holds [:(proj1 D),(proj2 D):] c= uparrow D

proof end;

scheme :: YELLOW_3:sch 6

Kappa2DS{ F_{1}() -> non empty RelStr , F_{2}() -> non empty RelStr , F_{3}() -> non empty RelStr , F_{4}( set , set ) -> set } :

Kappa2DS{ F

ex f being Function of [:F_{1}(),F_{2}():],F_{3}() st

for x being Element of F_{1}()

for y being Element of F_{2}() holds f . (x,y) = F_{4}(x,y)

providedfor x being Element of F

for y being Element of F

A1:
for x being Element of F_{1}()

for y being Element of F_{2}() holds F_{4}(x,y) is Element of F_{3}()

for y being Element of F

proof end;