:: by Grzegorz Bancerek

::

:: Received January 15, 1997

:: Copyright (c) 1997-2016 Association of Mizar Users

scheme :: WAYBEL10:sch 2

RelstrEq{ F_{1}() -> non empty RelStr , F_{2}() -> non empty RelStr , P_{1}[ object ], P_{2}[ set , set ] } :

RelstrEq{ F

RelStr(# the carrier of F_{1}(), the InternalRel of F_{1}() #) = RelStr(# the carrier of F_{2}(), the InternalRel of F_{2}() #)

provided
A1:
for x being object holds

( x is Element of F_{1}() iff P_{1}[x] )
and

A2: for x being object holds

( x is Element of F_{2}() iff P_{1}[x] )
and

A3: for a, b being Element of F_{1}() holds

( a <= b iff P_{2}[a,b] )
and

A4: for a, b being Element of F_{2}() holds

( a <= b iff P_{2}[a,b] )

( x is Element of F

A2: for x being object holds

( x is Element of F

A3: for a, b being Element of F

( a <= b iff P

A4: for a, b being Element of F

( a <= b iff P

proof end;

scheme :: WAYBEL10:sch 3

SubrelstrEq1{ F_{1}() -> non empty RelStr , F_{2}() -> non empty full SubRelStr of F_{1}(), F_{3}() -> non empty full SubRelStr of F_{1}(), P_{1}[ object ] } :

SubrelstrEq1{ F

RelStr(# the carrier of F_{2}(), the InternalRel of F_{2}() #) = RelStr(# the carrier of F_{3}(), the InternalRel of F_{3}() #)

provided
A1:
for x being object holds

( x is Element of F_{2}() iff P_{1}[x] )
and

A2: for x being object holds

( x is Element of F_{3}() iff P_{1}[x] )

( x is Element of F

A2: for x being object holds

( x is Element of F

proof end;

scheme :: WAYBEL10:sch 4

SubrelstrEq2{ F_{1}() -> non empty RelStr , F_{2}() -> non empty full SubRelStr of F_{1}(), F_{3}() -> non empty full SubRelStr of F_{1}(), P_{1}[ object ] } :

SubrelstrEq2{ F

RelStr(# the carrier of F_{2}(), the InternalRel of F_{2}() #) = RelStr(# the carrier of F_{3}(), the InternalRel of F_{3}() #)

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

( x is Element of F_{2}() iff P_{1}[x] )
and

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

( x is Element of F_{3}() iff P_{1}[x] )

( x is Element of F

A2: for x being Element of F

( x is Element of F

proof end;

theorem Th1: :: WAYBEL10:1

for R, Q being Relation holds

( ( R c= Q implies R ~ c= Q ~ ) & ( R ~ c= Q ~ implies R c= Q ) & ( R ~ c= Q implies R c= Q ~ ) & ( R c= Q ~ implies R ~ c= Q ) )

( ( R c= Q implies R ~ c= Q ~ ) & ( R ~ c= Q ~ implies R c= Q ) & ( R ~ c= Q implies R c= Q ~ ) & ( R c= Q ~ implies R ~ c= Q ) )

proof end;

theorem Th2: :: WAYBEL10:2

for L, S being RelStr holds

( ( S is SubRelStr of L implies S opp is SubRelStr of L opp ) & ( S opp is SubRelStr of L opp implies S is SubRelStr of L ) & ( S opp is SubRelStr of L implies S is SubRelStr of L opp ) & ( S is SubRelStr of L opp implies S opp is SubRelStr of L ) )

( ( S is SubRelStr of L implies S opp is SubRelStr of L opp ) & ( S opp is SubRelStr of L opp implies S is SubRelStr of L ) & ( S opp is SubRelStr of L implies S is SubRelStr of L opp ) & ( S is SubRelStr of L opp implies S opp is SubRelStr of L ) )

proof end;

theorem Th3: :: WAYBEL10:3

for L, S being RelStr holds

( ( S is full SubRelStr of L implies S opp is full SubRelStr of L opp ) & ( S opp is full SubRelStr of L opp implies S is full SubRelStr of L ) & ( S opp is full SubRelStr of L implies S is full SubRelStr of L opp ) & ( S is full SubRelStr of L opp implies S opp is full SubRelStr of L ) )

( ( S is full SubRelStr of L implies S opp is full SubRelStr of L opp ) & ( S opp is full SubRelStr of L opp implies S is full SubRelStr of L ) & ( S opp is full SubRelStr of L implies S is full SubRelStr of L opp ) & ( S is full SubRelStr of L opp implies S opp is full SubRelStr of L ) )

proof end;

definition

let L be RelStr ;

let S be full SubRelStr of L;

:: original: ~

redefine func S opp -> strict full SubRelStr of L opp ;

coherence

S ~ is strict full SubRelStr of L opp by Th3;

end;
let S be full SubRelStr of L;

:: original: ~

redefine func S opp -> strict full SubRelStr of L opp ;

coherence

S ~ is strict full SubRelStr of L opp by Th3;

registration
end;

registration

let S be RelStr ;

let T be non empty reflexive RelStr ;

ex b_{1} being Function of S,T st b_{1} is monotone

end;
let T be non empty reflexive RelStr ;

cluster Relation-like the carrier of S -defined the carrier of T -valued Function-like V24( the carrier of S) quasi_total monotone for Element of bool [: the carrier of S, the carrier of T:];

existence ex b

proof end;

registration

let L be non empty RelStr ;

for b_{1} being Function of L,L st b_{1} is projection holds

( b_{1} is monotone & b_{1} is idempotent )
by WAYBEL_1:def 13;

end;
cluster Function-like quasi_total projection -> idempotent monotone for Element of bool [: the carrier of L, the carrier of L:];

coherence for b

( b

registration

let S, T be non empty reflexive RelStr ;

let f be monotone Function of S,T;

coherence

corestr f is monotone

end;
let f be monotone Function of S,T;

coherence

corestr f is monotone

proof end;

registration

let L be non empty reflexive RelStr ;

coherence

( id L is sups-preserving & id L is infs-preserving )

end;
coherence

( id L is sups-preserving & id L is infs-preserving )

proof end;

theorem :: WAYBEL10:4

for L being RelStr

for S being Subset of L holds

( id S is Function of (subrelstr S),L & ( for f being Function of (subrelstr S),L st f = id S holds

f is monotone ) )

for S being Subset of L holds

( id S is Function of (subrelstr S),L & ( for f being Function of (subrelstr S),L st f = id S holds

f is monotone ) )

proof end;

registration

let L be non empty reflexive RelStr ;

ex b_{1} being Function of L,L st

( b_{1} is sups-preserving & b_{1} is infs-preserving & b_{1} is closure & b_{1} is kernel & b_{1} is V7() )

end;
cluster Relation-like the carrier of L -defined the carrier of L -valued Function-like V7() non empty V24( the carrier of L) quasi_total infs-preserving sups-preserving closure kernel for Element of bool [: the carrier of L, the carrier of L:];

existence ex b

( b

proof end;

theorem Th5: :: WAYBEL10:5

for L being non empty reflexive RelStr

for c being closure Function of L,L

for x being Element of L holds c . x >= x

for c being closure Function of L,L

for x being Element of L holds c . x >= x

proof end;

theorem Th6: :: WAYBEL10:6

for S, T being RelStr

for R being SubRelStr of S

for f being Function of the carrier of S, the carrier of T holds

( f | R = f | the carrier of R & ( for x being set st x in the carrier of R holds

(f | R) . x = f . x ) )

for R being SubRelStr of S

for f being Function of the carrier of S, the carrier of T holds

( f | R = f | the carrier of R & ( for x being set st x in the carrier of R holds

(f | R) . x = f . x ) )

proof end;

theorem Th7: :: WAYBEL10:7

for S, T being RelStr

for f being Function of S,T st f is one-to-one holds

for R being SubRelStr of S holds f | R is one-to-one

for f being Function of S,T st f is one-to-one holds

for R being SubRelStr of S holds f | R is one-to-one

proof end;

registration

let S, T be non empty reflexive RelStr ;

let f be monotone Function of S,T;

let R be SubRelStr of S;

coherence

f | R is monotone

end;
let f be monotone Function of S,T;

let R be SubRelStr of S;

coherence

f | R is monotone

proof end;

theorem Th8: :: WAYBEL10:8

for S, T being non empty RelStr

for R being non empty SubRelStr of S

for f being Function of S,T

for g being Function of T,S st f is V7() & g = f " holds

( g | (Image (f | R)) is Function of (Image (f | R)),R & g | (Image (f | R)) = (f | R) " )

for R being non empty SubRelStr of S

for f being Function of S,T

for g being Function of T,S st f is V7() & g = f " holds

( g | (Image (f | R)) is Function of (Image (f | R)),R & g | (Image (f | R)) = (f | R) " )

proof end;

registration

let S be RelStr ;

let T be non empty reflexive RelStr ;

coherence

not MonMaps (S,T) is empty

end;
let T be non empty reflexive RelStr ;

coherence

not MonMaps (S,T) is empty

proof end;

theorem Th9: :: WAYBEL10:9

for S being RelStr

for T being non empty reflexive RelStr

for x being set holds

( x is Element of (MonMaps (S,T)) iff x is monotone Function of S,T )

for T being non empty reflexive RelStr

for x being set holds

( x is Element of (MonMaps (S,T)) iff x is monotone Function of S,T )

proof end;

definition

let L be non empty reflexive RelStr ;

ex b_{1} being non empty strict full SubRelStr of MonMaps (L,L) st

for f being Function of L,L holds

( f is Element of b_{1} iff f is closure )

uniqueness

for b_{1}, b_{2} being non empty strict full SubRelStr of MonMaps (L,L) st ( for f being Function of L,L holds

( f is Element of b_{1} iff f is closure ) ) & ( for f being Function of L,L holds

( f is Element of b_{2} iff f is closure ) ) holds

b_{1} = b_{2};

end;
func ClOpers L -> non empty strict full SubRelStr of MonMaps (L,L) means :Def1: :: WAYBEL10:def 1

for f being Function of L,L holds

( f is Element of it iff f is closure );

existence for f being Function of L,L holds

( f is Element of it iff f is closure );

ex b

for f being Function of L,L holds

( f is Element of b

proof end;

correctness uniqueness

for b

( f is Element of b

( f is Element of b

b

proof end;

:: deftheorem Def1 defines ClOpers WAYBEL10:def 1 :

for L being non empty reflexive RelStr

for b_{2} being non empty strict full SubRelStr of MonMaps (L,L) holds

( b_{2} = ClOpers L iff for f being Function of L,L holds

( f is Element of b_{2} iff f is closure ) );

for L being non empty reflexive RelStr

for b

( b

( f is Element of b

theorem Th11: :: WAYBEL10:11

for X being set

for L being non empty RelStr

for f, g being Function of X, the carrier of L

for x, y being Element of (L |^ X) st x = f & y = g holds

( x <= y iff f <= g )

for L being non empty RelStr

for f, g being Function of X, the carrier of L

for x, y being Element of (L |^ X) st x = f & y = g holds

( x <= y iff f <= g )

proof end;

theorem Th12: :: WAYBEL10:12

for L being complete LATTICE

for c1, c2 being Function of L,L

for x, y being Element of (ClOpers L) st x = c1 & y = c2 holds

( x <= y iff c1 <= c2 )

for c1, c2 being Function of L,L

for x, y being Element of (ClOpers L) st x = c1 & y = c2 holds

( x <= y iff c1 <= c2 )

proof end;

theorem Th13: :: WAYBEL10:13

for L being reflexive RelStr

for S1, S2 being full SubRelStr of L st the carrier of S1 c= the carrier of S2 holds

S1 is SubRelStr of S2

for S1, S2 being full SubRelStr of L st the carrier of S1 c= the carrier of S2 holds

S1 is SubRelStr of S2

proof end;

theorem Th14: :: WAYBEL10:14

for L being complete LATTICE

for c1, c2 being closure Function of L,L holds

( c1 <= c2 iff Image c2 is SubRelStr of Image c1 )

for c1, c2 being closure Function of L,L holds

( c1 <= c2 iff Image c2 is SubRelStr of Image c1 )

proof end;

definition

let L be RelStr ;

ex b_{1} being non empty strict RelStr st

( ( for x being object holds

( x is Element of b_{1} iff x is strict SubRelStr of L ) ) & ( for a, b being Element of b_{1} holds

( a <= b iff ex R being RelStr st

( b = R & a is SubRelStr of R ) ) ) )

uniqueness

for b_{1}, b_{2} being non empty strict RelStr st ( for x being object holds

( x is Element of b_{1} iff x is strict SubRelStr of L ) ) & ( for a, b being Element of b_{1} holds

( a <= b iff ex R being RelStr st

( b = R & a is SubRelStr of R ) ) ) & ( for x being object holds

( x is Element of b_{2} iff x is strict SubRelStr of L ) ) & ( for a, b being Element of b_{2} holds

( a <= b iff ex R being RelStr st

( b = R & a is SubRelStr of R ) ) ) holds

b_{1} = b_{2};

end;
func Sub L -> non empty strict RelStr means :Def2: :: WAYBEL10:def 2

( ( for x being object holds

( x is Element of it iff x is strict SubRelStr of L ) ) & ( for a, b being Element of it holds

( a <= b iff ex R being RelStr st

( b = R & a is SubRelStr of R ) ) ) );

existence ( ( for x being object holds

( x is Element of it iff x is strict SubRelStr of L ) ) & ( for a, b being Element of it holds

( a <= b iff ex R being RelStr st

( b = R & a is SubRelStr of R ) ) ) );

ex b

( ( for x being object holds

( x is Element of b

( a <= b iff ex R being RelStr st

( b = R & a is SubRelStr of R ) ) ) )

proof end;

correctness uniqueness

for b

( x is Element of b

( a <= b iff ex R being RelStr st

( b = R & a is SubRelStr of R ) ) ) & ( for x being object holds

( x is Element of b

( a <= b iff ex R being RelStr st

( b = R & a is SubRelStr of R ) ) ) holds

b

proof end;

:: deftheorem Def2 defines Sub WAYBEL10:def 2 :

for L being RelStr

for b_{2} being non empty strict RelStr holds

( b_{2} = Sub L iff ( ( for x being object holds

( x is Element of b_{2} iff x is strict SubRelStr of L ) ) & ( for a, b being Element of b_{2} holds

( a <= b iff ex R being RelStr st

( b = R & a is SubRelStr of R ) ) ) ) );

for L being RelStr

for b

( b

( x is Element of b

( a <= b iff ex R being RelStr st

( b = R & a is SubRelStr of R ) ) ) ) );

theorem Th15: :: WAYBEL10:15

for L, R being RelStr

for x, y being Element of (Sub L) st y = R holds

( x <= y iff x is SubRelStr of R )

for x, y being Element of (Sub L) st y = R holds

( x <= y iff x is SubRelStr of R )

proof end;

registration

let L be RelStr ;

coherence

( Sub L is reflexive & Sub L is antisymmetric & Sub L is transitive )

end;
coherence

( Sub L is reflexive & Sub L is antisymmetric & Sub L is transitive )

proof end;

registration

let L be complete LATTICE;

coherence

for b_{1} being SubRelStr of L st b_{1} is infs-inheriting holds

not b_{1} is empty

for b_{1} being SubRelStr of L st b_{1} is sups-inheriting holds

not b_{1} is empty

end;
coherence

for b

not b

proof end;

coherence for b

not b

proof end;

notation
end;

registration

let L be non empty RelStr ;

coherence

( subrelstr ([#] L) is closure & subrelstr ([#] L) is sups-inheriting )

end;
coherence

( subrelstr ([#] L) is closure & subrelstr ([#] L) is sups-inheriting )

proof end;

definition

let L be non empty RelStr ;

ex b_{1} being non empty strict full SubRelStr of Sub L st

for R being strict SubRelStr of L holds

( R is Element of b_{1} iff ( R is infs-inheriting & R is full ) )

uniqueness

for b_{1}, b_{2} being non empty strict full SubRelStr of Sub L st ( for R being strict SubRelStr of L holds

( R is Element of b_{1} iff ( R is infs-inheriting & R is full ) ) ) & ( for R being strict SubRelStr of L holds

( R is Element of b_{2} iff ( R is infs-inheriting & R is full ) ) ) holds

b_{1} = b_{2};

end;
func ClosureSystems L -> non empty strict full SubRelStr of Sub L means :Def3: :: WAYBEL10:def 3

for R being strict SubRelStr of L holds

( R is Element of it iff ( R is infs-inheriting & R is full ) );

existence for R being strict SubRelStr of L holds

( R is Element of it iff ( R is infs-inheriting & R is full ) );

ex b

for R being strict SubRelStr of L holds

( R is Element of b

proof end;

correctness uniqueness

for b

( R is Element of b

( R is Element of b

b

proof end;

:: deftheorem Def3 defines ClosureSystems WAYBEL10:def 3 :

for L being non empty RelStr

for b_{2} being non empty strict full SubRelStr of Sub L holds

( b_{2} = ClosureSystems L iff for R being strict SubRelStr of L holds

( R is Element of b_{2} iff ( R is infs-inheriting & R is full ) ) );

for L being non empty RelStr

for b

( b

( R is Element of b

theorem Th16: :: WAYBEL10:16

for L being non empty RelStr

for x being object holds

( x is Element of (ClosureSystems L) iff x is strict closure System of L )

for x being object holds

( x is Element of (ClosureSystems L) iff x is strict closure System of L )

proof end;

theorem Th17: :: WAYBEL10:17

for L being non empty RelStr

for R being RelStr

for x, y being Element of (ClosureSystems L) st y = R holds

( x <= y iff x is SubRelStr of R )

for R being RelStr

for x, y being Element of (ClosureSystems L) st y = R holds

( x <= y iff x is SubRelStr of R )

proof end;

registration

let L be non empty Poset;

let h be closure Function of L,L;

coherence

Image h is closure by WAYBEL_1:53;

end;
let h be closure Function of L,L;

coherence

Image h is closure by WAYBEL_1:53;

definition

let L be non empty Poset;

ex b_{1} being Function of (ClOpers L),((ClosureSystems L) opp) st

for c being closure Function of L,L holds b_{1} . c = Image c

uniqueness

for b_{1}, b_{2} being Function of (ClOpers L),((ClosureSystems L) opp) st ( for c being closure Function of L,L holds b_{1} . c = Image c ) & ( for c being closure Function of L,L holds b_{2} . c = Image c ) holds

b_{1} = b_{2};

end;
func ClImageMap L -> Function of (ClOpers L),((ClosureSystems L) opp) means :Def4: :: WAYBEL10:def 4

for c being closure Function of L,L holds it . c = Image c;

existence for c being closure Function of L,L holds it . c = Image c;

ex b

for c being closure Function of L,L holds b

proof end;

correctness uniqueness

for b

b

proof end;

:: deftheorem Def4 defines ClImageMap WAYBEL10:def 4 :

for L being non empty Poset

for b_{2} being Function of (ClOpers L),((ClosureSystems L) opp) holds

( b_{2} = ClImageMap L iff for c being closure Function of L,L holds b_{2} . c = Image c );

for L being non empty Poset

for b

( b

definition

let L be non empty RelStr ;

let S be SubRelStr of L;

ex b_{1} being Function of L,L st

for x being Element of L holds b_{1} . x = "/\" (((uparrow x) /\ the carrier of S),L)

for b_{1}, b_{2} being Function of L,L st ( for x being Element of L holds b_{1} . x = "/\" (((uparrow x) /\ the carrier of S),L) ) & ( for x being Element of L holds b_{2} . x = "/\" (((uparrow x) /\ the carrier of S),L) ) holds

b_{1} = b_{2}

end;
let S be SubRelStr of L;

func closure_op S -> Function of L,L means :Def5: :: WAYBEL10:def 5

for x being Element of L holds it . x = "/\" (((uparrow x) /\ the carrier of S),L);

existence for x being Element of L holds it . x = "/\" (((uparrow x) /\ the carrier of S),L);

ex b

for x being Element of L holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines closure_op WAYBEL10:def 5 :

for L being non empty RelStr

for S being SubRelStr of L

for b_{3} being Function of L,L holds

( b_{3} = closure_op S iff for x being Element of L holds b_{3} . x = "/\" (((uparrow x) /\ the carrier of S),L) );

for L being non empty RelStr

for S being SubRelStr of L

for b

( b

registration

let L be complete LATTICE;

let S be closure System of L;

coherence

closure_op S is closure

end;
let S be closure System of L;

coherence

closure_op S is closure

proof end;

theorem Th18: :: WAYBEL10:18

for L being complete LATTICE

for S being closure System of L holds Image (closure_op S) = RelStr(# the carrier of S, the InternalRel of S #)

for S being closure System of L holds Image (closure_op S) = RelStr(# the carrier of S, the InternalRel of S #)

proof end;

theorem Th20: :: WAYBEL10:20

for L being complete LATTICE holds (ClImageMap L) " is Function of ((ClosureSystems L) opp),(ClOpers L)

proof end;

theorem Th21: :: WAYBEL10:21

for L being complete LATTICE

for S being strict closure System of L holds ((ClImageMap L) ") . S = closure_op S

for S being strict closure System of L holds ((ClImageMap L) ") . S = closure_op S

proof end;

registration
end;

:: and subalgebras

theorem Th23: :: WAYBEL10:23

for L being RelStr

for S being full SubRelStr of L

for X being Subset of S holds

( ( X is directed Subset of L implies X is directed ) & ( X is filtered Subset of L implies X is filtered ) )

for S being full SubRelStr of L

for X being Subset of S holds

( ( X is directed Subset of L implies X is directed ) & ( X is filtered Subset of L implies X is filtered ) )

proof end;

:: Corollary 3.14, p. 24

theorem Th24: :: WAYBEL10:24

for L being complete LATTICE

for S being closure System of L holds

( closure_op S is directed-sups-preserving iff S is directed-sups-inheriting )

for S being closure System of L holds

( closure_op S is directed-sups-preserving iff S is directed-sups-inheriting )

proof end;

theorem :: WAYBEL10:25

for L being complete LATTICE

for h being closure Function of L,L holds

( h is directed-sups-preserving iff Image h is directed-sups-inheriting )

for h being closure Function of L,L holds

( h is directed-sups-preserving iff Image h is directed-sups-inheriting )

proof end;

registration

let L be complete LATTICE;

let S be closure directed-sups-inheriting System of L;

coherence

closure_op S is directed-sups-preserving by Th24;

end;
let S be closure directed-sups-inheriting System of L;

coherence

closure_op S is directed-sups-preserving by Th24;

registration

let L be complete LATTICE;

let h be directed-sups-preserving closure Function of L,L;

coherence

Image h is directed-sups-inheriting

end;
let h be directed-sups-preserving closure Function of L,L;

coherence

Image h is directed-sups-inheriting

proof end;

definition

let L be non empty reflexive RelStr ;

ex b_{1} being non empty strict full SubRelStr of ClOpers L st

for f being closure Function of L,L holds

( f is Element of b_{1} iff f is directed-sups-preserving )

uniqueness

for b_{1}, b_{2} being non empty strict full SubRelStr of ClOpers L st ( for f being closure Function of L,L holds

( f is Element of b_{1} iff f is directed-sups-preserving ) ) & ( for f being closure Function of L,L holds

( f is Element of b_{2} iff f is directed-sups-preserving ) ) holds

b_{1} = b_{2};

end;
func DsupClOpers L -> non empty strict full SubRelStr of ClOpers L means :Def6: :: WAYBEL10:def 6

for f being closure Function of L,L holds

( f is Element of it iff f is directed-sups-preserving );

existence for f being closure Function of L,L holds

( f is Element of it iff f is directed-sups-preserving );

ex b

for f being closure Function of L,L holds

( f is Element of b

proof end;

correctness uniqueness

for b

( f is Element of b

( f is Element of b

b

proof end;

:: deftheorem Def6 defines DsupClOpers WAYBEL10:def 6 :

for L being non empty reflexive RelStr

for b_{2} being non empty strict full SubRelStr of ClOpers L holds

( b_{2} = DsupClOpers L iff for f being closure Function of L,L holds

( f is Element of b_{2} iff f is directed-sups-preserving ) );

for L being non empty reflexive RelStr

for b

( b

( f is Element of b

theorem Th26: :: WAYBEL10:26

for L being non empty reflexive RelStr

for x being set holds

( x is Element of (DsupClOpers L) iff x is directed-sups-preserving closure Function of L,L )

for x being set holds

( x is Element of (DsupClOpers L) iff x is directed-sups-preserving closure Function of L,L )

proof end;

definition

let L be non empty RelStr ;

ex b_{1} being non empty strict full SubRelStr of ClosureSystems L st

for R being strict closure System of L holds

( R is Element of b_{1} iff R is directed-sups-inheriting )

uniqueness

for b_{1}, b_{2} being non empty strict full SubRelStr of ClosureSystems L st ( for R being strict closure System of L holds

( R is Element of b_{1} iff R is directed-sups-inheriting ) ) & ( for R being strict closure System of L holds

( R is Element of b_{2} iff R is directed-sups-inheriting ) ) holds

b_{1} = b_{2};

end;
func Subalgebras L -> non empty strict full SubRelStr of ClosureSystems L means :Def7: :: WAYBEL10:def 7

for R being strict closure System of L holds

( R is Element of it iff R is directed-sups-inheriting );

existence for R being strict closure System of L holds

( R is Element of it iff R is directed-sups-inheriting );

ex b

for R being strict closure System of L holds

( R is Element of b

proof end;

correctness uniqueness

for b

( R is Element of b

( R is Element of b

b

proof end;

:: deftheorem Def7 defines Subalgebras WAYBEL10:def 7 :

for L being non empty RelStr

for b_{2} being non empty strict full SubRelStr of ClosureSystems L holds

( b_{2} = Subalgebras L iff for R being strict closure System of L holds

( R is Element of b_{2} iff R is directed-sups-inheriting ) );

for L being non empty RelStr

for b

( b

( R is Element of b

theorem Th27: :: WAYBEL10:27

for L being non empty RelStr

for x being object holds

( x is Element of (Subalgebras L) iff x is strict closure directed-sups-inheriting System of L )

for x being object holds

( x is Element of (Subalgebras L) iff x is strict closure directed-sups-inheriting System of L )

proof end;

registration

let L be complete LATTICE;

coherence

corestr ((ClImageMap L) | (DsupClOpers L)) is isomorphic

end;
coherence

corestr ((ClImageMap L) | (DsupClOpers L)) is isomorphic

proof end;