:: by Artur Korni{\l}owicz

::

:: Received March 27, 1998

:: Copyright (c) 1998-2021 Association of Mizar Users

registration
end;

registration
end;

theorem :: YELLOW10:1

for S, T being non empty RelStr st [:S,T:] is upper-bounded holds

( S is upper-bounded & T is upper-bounded )

( S is upper-bounded & T is upper-bounded )

proof end;

theorem :: YELLOW10:2

for S, T being non empty RelStr st [:S,T:] is lower-bounded holds

( S is lower-bounded & T is lower-bounded )

( S is lower-bounded & T is lower-bounded )

proof end;

theorem Th4: :: YELLOW10:4

for S, T being non empty antisymmetric lower-bounded RelStr holds Bottom [:S,T:] = [(Bottom S),(Bottom T)]

proof end;

theorem Th5: :: YELLOW10:5

for S, T being non empty antisymmetric lower-bounded RelStr

for 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))]

for 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 end;

theorem :: YELLOW10:6

for S, T being non empty antisymmetric upper-bounded RelStr

for 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))]

for 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 end;

theorem :: YELLOW10:7

for S, T being non empty RelStr

for 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)} ) )

for 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 end;

theorem :: YELLOW10:8

for S, T being non empty RelStr

for 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)} ) )

for 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 end;

theorem :: YELLOW10:9

for S, T being non empty RelStr

for 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)} ) )

for 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 end;

theorem :: YELLOW10:10

for S, T being non empty RelStr

for 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)} ) )

for 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 end;

theorem :: YELLOW10:11

for S, T being non empty antisymmetric RelStr

for 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 ) )

for 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 end;

theorem :: YELLOW10:12

for S, T being non empty antisymmetric RelStr

for 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 ) )

for 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 end;

theorem Th13: :: YELLOW10:13

for S, T being antisymmetric with_infima RelStr

for x, y being Element of [:S,T:] holds

( (x "/\" y) `1 = (x `1) "/\" (y `1) & (x "/\" y) `2 = (x `2) "/\" (y `2) )

for x, y being Element of [:S,T:] holds

( (x "/\" y) `1 = (x `1) "/\" (y `1) & (x "/\" y) `2 = (x `2) "/\" (y `2) )

proof end;

theorem Th14: :: YELLOW10:14

for S, T being antisymmetric with_suprema RelStr

for x, y being Element of [:S,T:] holds

( (x "\/" y) `1 = (x `1) "\/" (y `1) & (x "\/" y) `2 = (x `2) "\/" (y `2) )

for x, y being Element of [:S,T:] holds

( (x "\/" y) `1 = (x `1) "\/" (y `1) & (x "\/" y) `2 = (x `2) "\/" (y `2) )

proof end;

theorem Th15: :: YELLOW10:15

for S, T being antisymmetric with_infima RelStr

for x1, y1 being Element of S

for x2, y2 being Element of T holds [(x1 "/\" y1),(x2 "/\" y2)] = [x1,x2] "/\" [y1,y2]

for x1, y1 being Element of S

for x2, y2 being Element of T holds [(x1 "/\" y1),(x2 "/\" y2)] = [x1,x2] "/\" [y1,y2]

proof end;

theorem Th16: :: YELLOW10:16

for S, T being antisymmetric with_suprema RelStr

for x1, y1 being Element of S

for x2, y2 being Element of T holds [(x1 "\/" y1),(x2 "\/" y2)] = [x1,x2] "\/" [y1,y2]

for x1, y1 being Element of S

for x2, y2 being Element of T holds [(x1 "\/" y1),(x2 "\/" y2)] = [x1,x2] "\/" [y1,y2]

proof end;

definition

let S be antisymmetric with_suprema with_infima RelStr ;

let x, y be Element of S;

:: original: is_a_complement_of

redefine pred y is_a_complement_of x;

symmetry

for y, x being Element of S st R55(S,b_{2},b_{1}) holds

R55(S,b_{1},b_{2})

end;
let x, y be Element of S;

:: original: is_a_complement_of

redefine pred y is_a_complement_of x;

symmetry

for y, x being Element of S st R55(S,b

R55(S,b

proof end;

theorem Th17: :: YELLOW10:17

for S, T being antisymmetric bounded with_suprema with_infima RelStr

for 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 ) )

for 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 end;

theorem Th18: :: YELLOW10:18

for S, T being non empty reflexive antisymmetric up-complete RelStr

for a, c being Element of S

for b, d being Element of T st [a,b] << [c,d] holds

( a << c & b << d )

for a, c being Element of S

for b, d being Element of T st [a,b] << [c,d] holds

( a << c & b << d )

proof end;

theorem Th19: :: YELLOW10:19

for S, T being non empty up-complete Poset

for a, c being Element of S

for b, d being Element of T holds

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

for a, c being Element of S

for b, d being Element of T holds

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

proof end;

theorem Th20: :: YELLOW10:20

for S, T being non empty reflexive antisymmetric up-complete RelStr

for x, y being Element of [:S,T:] st x << y holds

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

for x, y being Element of [:S,T:] st x << y holds

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

proof end;

theorem Th21: :: YELLOW10:21

for S, T being non empty up-complete Poset

for x, y being Element of [:S,T:] holds

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

for x, y being Element of [:S,T:] holds

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

proof end;

theorem Th22: :: YELLOW10:22

for S, T being non empty reflexive antisymmetric up-complete RelStr

for x being Element of [:S,T:] st x is compact holds

( x `1 is compact & x `2 is compact )

for x being Element of [:S,T:] st x is compact holds

( x `1 is compact & x `2 is compact )

proof end;

theorem Th23: :: YELLOW10:23

for S, T being non empty up-complete Poset

for x being Element of [:S,T:] st x `1 is compact & x `2 is compact holds

x is compact

for x being Element of [:S,T:] st x `1 is compact & x `2 is compact holds

x is compact

proof end;

theorem Th24: :: YELLOW10:24

for S, T being antisymmetric with_infima RelStr

for X, Y being Subset of [:S,T:] holds

( proj1 (X "/\" Y) = (proj1 X) "/\" (proj1 Y) & proj2 (X "/\" Y) = (proj2 X) "/\" (proj2 Y) )

for X, Y being Subset of [:S,T:] holds

( proj1 (X "/\" Y) = (proj1 X) "/\" (proj1 Y) & proj2 (X "/\" Y) = (proj2 X) "/\" (proj2 Y) )

proof end;

theorem :: YELLOW10:25

for S, T being antisymmetric with_suprema RelStr

for X, Y being Subset of [:S,T:] holds

( proj1 (X "\/" Y) = (proj1 X) "\/" (proj1 Y) & proj2 (X "\/" Y) = (proj2 X) "\/" (proj2 Y) )

for X, Y being Subset of [:S,T:] holds

( proj1 (X "\/" Y) = (proj1 X) "\/" (proj1 Y) & proj2 (X "\/" Y) = (proj2 X) "\/" (proj2 Y) )

proof end;

theorem :: YELLOW10:26

for S, T being RelStr

for X being Subset of [:S,T:] holds downarrow X c= [:(downarrow (proj1 X)),(downarrow (proj2 X)):]

for X being Subset of [:S,T:] holds downarrow X c= [:(downarrow (proj1 X)),(downarrow (proj2 X)):]

proof end;

theorem :: YELLOW10:27

for S, T being RelStr

for X being Subset of S

for Y being Subset of T holds [:(downarrow X),(downarrow Y):] = downarrow [:X,Y:]

for X being Subset of S

for Y being Subset of T holds [:(downarrow X),(downarrow Y):] = downarrow [:X,Y:]

proof end;

theorem Th28: :: YELLOW10:28

for S, T being RelStr

for X being Subset of [:S,T:] holds

( proj1 (downarrow X) c= downarrow (proj1 X) & proj2 (downarrow X) c= downarrow (proj2 X) )

for X being Subset of [:S,T:] holds

( proj1 (downarrow X) c= downarrow (proj1 X) & proj2 (downarrow X) c= downarrow (proj2 X) )

proof end;

theorem :: YELLOW10:29

for S being RelStr

for T being reflexive RelStr

for X being Subset of [:S,T:] holds proj1 (downarrow X) = downarrow (proj1 X)

for T being reflexive RelStr

for X being Subset of [:S,T:] holds proj1 (downarrow X) = downarrow (proj1 X)

proof end;

theorem :: YELLOW10:30

for S being reflexive RelStr

for T being RelStr

for X being Subset of [:S,T:] holds proj2 (downarrow X) = downarrow (proj2 X)

for T being RelStr

for X being Subset of [:S,T:] holds proj2 (downarrow X) = downarrow (proj2 X)

proof end;

theorem :: YELLOW10:31

for S, T being RelStr

for X being Subset of [:S,T:] holds uparrow X c= [:(uparrow (proj1 X)),(uparrow (proj2 X)):]

for X being Subset of [:S,T:] holds uparrow X c= [:(uparrow (proj1 X)),(uparrow (proj2 X)):]

proof end;

theorem :: YELLOW10:32

for S, T being RelStr

for X being Subset of S

for Y being Subset of T holds [:(uparrow X),(uparrow Y):] = uparrow [:X,Y:]

for X being Subset of S

for Y being Subset of T holds [:(uparrow X),(uparrow Y):] = uparrow [:X,Y:]

proof end;

theorem Th33: :: YELLOW10:33

for S, T being RelStr

for X being Subset of [:S,T:] holds

( proj1 (uparrow X) c= uparrow (proj1 X) & proj2 (uparrow X) c= uparrow (proj2 X) )

for X being Subset of [:S,T:] holds

( proj1 (uparrow X) c= uparrow (proj1 X) & proj2 (uparrow X) c= uparrow (proj2 X) )

proof end;

theorem :: YELLOW10:34

for S being RelStr

for T being reflexive RelStr

for X being Subset of [:S,T:] holds proj1 (uparrow X) = uparrow (proj1 X)

for T being reflexive RelStr

for X being Subset of [:S,T:] holds proj1 (uparrow X) = uparrow (proj1 X)

proof end;

theorem :: YELLOW10:35

for S being reflexive RelStr

for T being RelStr

for X being Subset of [:S,T:] holds proj2 (uparrow X) = uparrow (proj2 X)

for T being RelStr

for X being Subset of [:S,T:] holds proj2 (uparrow X) = uparrow (proj2 X)

proof end;

theorem :: YELLOW10:36

for S, T being non empty RelStr

for s being Element of S

for t being Element of T holds [:(downarrow s),(downarrow t):] = downarrow [s,t]

for s being Element of S

for t being Element of T holds [:(downarrow s),(downarrow t):] = downarrow [s,t]

proof end;

theorem Th37: :: YELLOW10:37

for S, T being non empty RelStr

for x being Element of [:S,T:] holds

( proj1 (downarrow x) c= downarrow (x `1) & proj2 (downarrow x) c= downarrow (x `2) )

for x being Element of [:S,T:] holds

( proj1 (downarrow x) c= downarrow (x `1) & proj2 (downarrow x) c= downarrow (x `2) )

proof end;

theorem :: YELLOW10:38

for S being non empty RelStr

for T being non empty reflexive RelStr

for x being Element of [:S,T:] holds proj1 (downarrow x) = downarrow (x `1)

for T being non empty reflexive RelStr

for x being Element of [:S,T:] holds proj1 (downarrow x) = downarrow (x `1)

proof end;

theorem :: YELLOW10:39

for S being non empty reflexive RelStr

for T being non empty RelStr

for x being Element of [:S,T:] holds proj2 (downarrow x) = downarrow (x `2)

for T being non empty RelStr

for x being Element of [:S,T:] holds proj2 (downarrow x) = downarrow (x `2)

proof end;

theorem :: YELLOW10:40

for S, T being non empty RelStr

for s being Element of S

for t being Element of T holds [:(uparrow s),(uparrow t):] = uparrow [s,t]

for s being Element of S

for t being Element of T holds [:(uparrow s),(uparrow t):] = uparrow [s,t]

proof end;

theorem Th41: :: YELLOW10:41

for S, T being non empty RelStr

for x being Element of [:S,T:] holds

( proj1 (uparrow x) c= uparrow (x `1) & proj2 (uparrow x) c= uparrow (x `2) )

for x being Element of [:S,T:] holds

( proj1 (uparrow x) c= uparrow (x `1) & proj2 (uparrow x) c= uparrow (x `2) )

proof end;

theorem :: YELLOW10:42

for S being non empty RelStr

for T being non empty reflexive RelStr

for x being Element of [:S,T:] holds proj1 (uparrow x) = uparrow (x `1)

for T being non empty reflexive RelStr

for x being Element of [:S,T:] holds proj1 (uparrow x) = uparrow (x `1)

proof end;

theorem :: YELLOW10:43

for S being non empty reflexive RelStr

for T being non empty RelStr

for x being Element of [:S,T:] holds proj2 (uparrow x) = uparrow (x `2)

for T being non empty RelStr

for x being Element of [:S,T:] holds proj2 (uparrow x) = uparrow (x `2)

proof end;

theorem Th44: :: YELLOW10:44

for S, T being non empty up-complete Poset

for s being Element of S

for t being Element of T holds [:(waybelow s),(waybelow t):] = waybelow [s,t]

for s being Element of S

for t being Element of T holds [:(waybelow s),(waybelow t):] = waybelow [s,t]

proof end;

theorem Th45: :: YELLOW10:45

for S, T being non empty reflexive antisymmetric up-complete RelStr

for x being Element of [:S,T:] holds

( proj1 (waybelow x) c= waybelow (x `1) & proj2 (waybelow x) c= waybelow (x `2) )

for x being Element of [:S,T:] holds

( proj1 (waybelow x) c= waybelow (x `1) & proj2 (waybelow x) c= waybelow (x `2) )

proof end;

theorem Th46: :: YELLOW10:46

for S being non empty up-complete Poset

for T being non empty lower-bounded up-complete Poset

for x being Element of [:S,T:] holds proj1 (waybelow x) = waybelow (x `1)

for T being non empty lower-bounded up-complete Poset

for x being Element of [:S,T:] holds proj1 (waybelow x) = waybelow (x `1)

proof end;

theorem Th47: :: YELLOW10:47

for S being non empty lower-bounded up-complete Poset

for T being non empty up-complete Poset

for x being Element of [:S,T:] holds proj2 (waybelow x) = waybelow (x `2)

for T being non empty up-complete Poset

for x being Element of [:S,T:] holds proj2 (waybelow x) = waybelow (x `2)

proof end;

theorem :: YELLOW10:48

for S, T being non empty up-complete Poset

for s being Element of S

for t being Element of T holds [:(wayabove s),(wayabove t):] = wayabove [s,t]

for s being Element of S

for t being Element of T holds [:(wayabove s),(wayabove t):] = wayabove [s,t]

proof end;

theorem :: YELLOW10:49

for S, T being non empty reflexive antisymmetric up-complete RelStr

for x being Element of [:S,T:] holds

( proj1 (wayabove x) c= wayabove (x `1) & proj2 (wayabove x) c= wayabove (x `2) )

for x being Element of [:S,T:] holds

( proj1 (wayabove x) c= wayabove (x `1) & proj2 (wayabove x) c= wayabove (x `2) )

proof end;

theorem Th50: :: YELLOW10:50

for S, T being non empty up-complete Poset

for s being Element of S

for t being Element of T holds [:(compactbelow s),(compactbelow t):] = compactbelow [s,t]

for s being Element of S

for t being Element of T holds [:(compactbelow s),(compactbelow t):] = compactbelow [s,t]

proof end;

theorem Th51: :: YELLOW10:51

for S, T being non empty reflexive antisymmetric up-complete RelStr

for x being Element of [:S,T:] holds

( proj1 (compactbelow x) c= compactbelow (x `1) & proj2 (compactbelow x) c= compactbelow (x `2) )

for x being Element of [:S,T:] holds

( proj1 (compactbelow x) c= compactbelow (x `1) & proj2 (compactbelow x) c= compactbelow (x `2) )

proof end;

theorem Th52: :: YELLOW10:52

for S being non empty up-complete Poset

for T being non empty lower-bounded up-complete Poset

for x being Element of [:S,T:] holds proj1 (compactbelow x) = compactbelow (x `1)

for T being non empty lower-bounded up-complete Poset

for x being Element of [:S,T:] holds proj1 (compactbelow x) = compactbelow (x `1)

proof end;

theorem Th53: :: YELLOW10:53

for S being non empty lower-bounded up-complete Poset

for T being non empty up-complete Poset

for x being Element of [:S,T:] holds proj2 (compactbelow x) = compactbelow (x `2)

for T being non empty up-complete Poset

for x being Element of [:S,T:] holds proj2 (compactbelow x) = compactbelow (x `2)

proof end;

registration

let S be non empty reflexive RelStr ;

coherence

for b_{1} being Subset of S st b_{1} is empty holds

b_{1} is Open

end;
coherence

for b

b

proof end;

theorem :: YELLOW10:54

for S, T being non empty reflexive antisymmetric up-complete RelStr

for X being Subset of [:S,T:] st X is Open holds

( proj1 X is Open & proj2 X is Open )

for X being Subset of [:S,T:] st X is Open holds

( proj1 X is Open & proj2 X is Open )

proof end;

theorem :: YELLOW10:55

for S, T being non empty up-complete Poset

for X being Subset of S

for Y being Subset of T st X is Open & Y is Open holds

[:X,Y:] is Open

for X being Subset of S

for Y being Subset of T st X is Open & Y is Open holds

[:X,Y:] is Open

proof end;

theorem :: YELLOW10:56

for S, T being non empty reflexive antisymmetric up-complete RelStr

for X being Subset of [:S,T:] st X is inaccessible holds

( proj1 X is inaccessible & proj2 X is inaccessible )

for X being Subset of [:S,T:] st X is inaccessible holds

( proj1 X is inaccessible & proj2 X is inaccessible )

proof end;

theorem :: YELLOW10:57

for S, T being non empty reflexive antisymmetric up-complete RelStr

for X being upper Subset of S

for Y being upper Subset of T st X is inaccessible & Y is inaccessible holds

[:X,Y:] is inaccessible

for X being upper Subset of S

for Y being upper Subset of T st X is inaccessible & Y is inaccessible holds

[:X,Y:] is inaccessible

proof end;

theorem :: YELLOW10:58

for S, T being non empty reflexive antisymmetric up-complete RelStr

for X being Subset of S

for Y being Subset of T st [:X,Y:] is directly_closed holds

( ( Y <> {} implies X is directly_closed ) & ( X <> {} implies Y is directly_closed ) )

for X being Subset of S

for 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 end;

theorem :: YELLOW10:59

for S, T being non empty reflexive antisymmetric up-complete RelStr

for X being Subset of S

for Y being Subset of T st X is directly_closed & Y is directly_closed holds

[:X,Y:] is directly_closed

for X being Subset of S

for Y being Subset of T st X is directly_closed & Y is directly_closed holds

[:X,Y:] is directly_closed

proof end;

theorem :: YELLOW10:60

for S, T being non empty reflexive antisymmetric up-complete RelStr

for X being Subset of [:S,T:] st X is property(S) holds

( proj1 X is property(S) & proj2 X is property(S) )

for X being Subset of [:S,T:] st X is property(S) holds

( proj1 X is property(S) & proj2 X is property(S) )

proof end;

theorem :: YELLOW10:61

for S, T being non empty up-complete Poset

for X being Subset of S

for Y being Subset of T st X is property(S) & Y is property(S) holds

[:X,Y:] is property(S)

for X being Subset of S

for Y being Subset of T st X is property(S) & Y is property(S) holds

[:X,Y:] is property(S)

proof end;

theorem Th62: :: YELLOW10:62

for S, T being non empty reflexive RelStr st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) & S is /\-complete holds

T is /\-complete

T is /\-complete

proof end;

registration

let S be non empty reflexive /\-complete RelStr ;

coherence

RelStr(# the carrier of S, the InternalRel of S #) is /\-complete by Th62;

end;
coherence

RelStr(# the carrier of S, the InternalRel of S #) is /\-complete by Th62;

registration
end;

theorem :: YELLOW10:63

for S, T being non empty reflexive RelStr st [:S,T:] is /\-complete holds

( S is /\-complete & T is /\-complete )

( S is /\-complete & T is /\-complete )

proof end;

registration

let S, T be non empty antisymmetric bounded complemented with_suprema with_infima RelStr ;

coherence

[:S,T:] is complemented

end;
coherence

[:S,T:] is complemented

proof end;

theorem :: YELLOW10:64

for S, T being antisymmetric bounded with_suprema with_infima RelStr st [:S,T:] is complemented holds

( S is complemented & T is complemented )

( S is complemented & T is complemented )

proof end;

registration

let S, T be non empty antisymmetric distributive with_suprema with_infima RelStr ;

coherence

[:S,T:] is distributive

end;
coherence

[:S,T:] is distributive

proof end;

theorem :: YELLOW10:65

for S being antisymmetric with_suprema with_infima RelStr

for T being reflexive antisymmetric with_suprema with_infima RelStr st [:S,T:] is distributive holds

S is distributive

for T being reflexive antisymmetric with_suprema with_infima RelStr st [:S,T:] is distributive holds

S is distributive

proof end;

theorem :: YELLOW10:66

for S being reflexive antisymmetric with_suprema with_infima RelStr

for T being antisymmetric with_suprema with_infima RelStr st [:S,T:] is distributive holds

T is distributive

for T being antisymmetric with_suprema with_infima RelStr st [:S,T:] is distributive holds

T is distributive

proof end;

registration
end;

theorem :: YELLOW10:67

for S, T being Semilattice st [:S,T:] is meet-continuous holds

( S is meet-continuous & T is meet-continuous )

( S is meet-continuous & T is meet-continuous )

proof end;

registration

let S, T be non empty up-complete /\-complete satisfying_axiom_of_approximation Poset;

coherence

[:S,T:] is satisfying_axiom_of_approximation

end;
coherence

[:S,T:] is satisfying_axiom_of_approximation

proof end;

registration
end;

theorem :: YELLOW10:68

for S, T being non empty lower-bounded up-complete Poset st [:S,T:] is continuous holds

( S is continuous & T is continuous )

( S is continuous & T is continuous )

proof end;

registration

let S, T be lower-bounded up-complete satisfying_axiom_K sup-Semilattice;

coherence

[:S,T:] is satisfying_axiom_K

end;
coherence

[:S,T:] is satisfying_axiom_K

proof end;

registration
end;

theorem Th69: :: YELLOW10:69

for S, T being non empty lower-bounded Poset st [:S,T:] is algebraic holds

( S is algebraic & T is algebraic )

( S is algebraic & T is algebraic )

proof end;

registration
end;

theorem :: YELLOW10:70

for S, T being lower-bounded LATTICE st [:S,T:] is arithmetic holds

( S is arithmetic & T is arithmetic )

( S is arithmetic & T is arithmetic )

proof end;