:: WAYBEL10 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

scheme :: WAYBEL10:sch 1
SubrelstrEx{ F1() -> non empty RelStr , P1[ set ], F2() -> set } :
ex S being non empty strict full SubRelStr of F1() st
for x being Element of F1() holds
( x is Element of S iff P1[x] )
provided
A1: P1[F2()] and
A2: F2() in the carrier of F1()
proof end;

scheme :: WAYBEL10:sch 2
RelstrEq{ F1() -> non empty RelStr , F2() -> non empty RelStr , P1[ set ], P2[ set , set ] } :
RelStr(# the carrier of F1(),the InternalRel of F1() #) = RelStr(# the carrier of F2(),the InternalRel of F2() #)
provided
A1: for x being set holds
( x is Element of F1() iff P1[x] ) and
A2: for x being set holds
( x is Element of F2() iff P1[x] ) and
A3: for a, b being Element of F1() holds
( a <= b iff P2[a,b] ) and
A4: for a, b being Element of F2() holds
( a <= b iff P2[a,b] )
proof end;

scheme :: WAYBEL10:sch 3
SubrelstrEq1{ F1() -> non empty RelStr , F2() -> non empty full SubRelStr of F1(), F3() -> non empty full SubRelStr of F1(), P1[ set ] } :
RelStr(# the carrier of F2(),the InternalRel of F2() #) = RelStr(# the carrier of F3(),the InternalRel of F3() #)
provided
A1: for x being set holds
( x is Element of F2() iff P1[x] ) and
A2: for x being set holds
( x is Element of F3() iff P1[x] )
proof end;

scheme :: WAYBEL10:sch 4
SubrelstrEq2{ F1() -> non empty RelStr , F2() -> non empty full SubRelStr of F1(), F3() -> non empty full SubRelStr of F1(), P1[ set ] } :
RelStr(# the carrier of F2(),the InternalRel of F2() #) = RelStr(# the carrier of F3(),the InternalRel of F3() #)
provided
A1: for x being Element of F1() holds
( x is Element of F2() iff P1[x] ) and
A2: for x being Element of F1() holds
( x is Element of F3() iff P1[x] )
proof end;

theorem Th1: :: WAYBEL10:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

theorem :: WAYBEL10:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th3: :: WAYBEL10:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

theorem Th4: :: WAYBEL10:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
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 Th4;
end;

registration
let X be set ;
let L be non empty RelStr ;
cluster K104(X,L) -> non-Empty ;
coherence
X --> L is non-Empty
proof end;
end;

registration
let S be RelStr ;
let T be non empty reflexive RelStr ;
cluster monotone Relation of the carrier of S,the carrier of T;
existence
ex b1 being Function of S,T st b1 is monotone
proof end;
end;

registration
let L be non empty RelStr ;
cluster projection -> idempotent monotone Relation of the carrier of L,the carrier of L;
coherence
for b1 being Function of L,L st b1 is projection holds
( b1 is monotone & b1 is idempotent )
by WAYBEL_1:def 13;
end;

registration
let S, T be non empty reflexive RelStr ;
let f be monotone Function of S,T;
cluster corestr f -> monotone ;
coherence
corestr f is monotone
proof end;
end;

registration
let L be 1-sorted ;
cluster id L -> one-to-one ;
coherence
id L is one-to-one
proof end;
end;

registration
let L be non empty reflexive RelStr ;
cluster id L -> idempotent infs-preserving sups-preserving ;
coherence
( id L is sups-preserving & id L is infs-preserving )
proof end;
end;

theorem :: WAYBEL10:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

registration
let L be non empty reflexive RelStr ;
cluster V5 idempotent monotone infs-preserving sups-preserving closure kernel Relation of the carrier of L,the carrier of L;
existence
ex b1 being Function of L,L st
( b1 is sups-preserving & b1 is infs-preserving & b1 is closure & b1 is kernel & b1 is one-to-one )
proof end;
end;

theorem Th6: :: WAYBEL10:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

definition
let S, T be 1-sorted ;
let f be Function of the carrier of S,the carrier of T;
let R be 1-sorted ;
assume A1: the carrier of R c= the carrier of S ;
func f | R -> Function of R,T equals :Def1: :: WAYBEL10:def 1
f | the carrier of R;
coherence
f | the carrier of R is Function of R,T
proof end;
correctness
;
end;

:: deftheorem Def1 defines | WAYBEL10:def 1 :
for S, T being 1-sorted
for f being Function of the carrier of S,the carrier of T
for R being 1-sorted st the carrier of R c= the carrier of S holds
f | R = f | the carrier of R;

theorem Th7: :: WAYBEL10:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

theorem Th8: :: WAYBEL10:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
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;
cluster f | R -> monotone ;
coherence
f | R is monotone
proof end;
end;

theorem Th9: :: WAYBEL10:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 one-to-one & 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 ;
cluster MonMaps S,T -> non empty ;
coherence
not MonMaps S,T is empty
proof end;
end;

theorem Th10: :: WAYBEL10:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

definition
let L be non empty reflexive RelStr ;
func ClOpers L -> non empty strict full SubRelStr of MonMaps L,L means :Def2: :: WAYBEL10:def 2
for f being Function of L,L holds
( f is Element of it iff f is closure );
existence
ex b1 being non empty strict full SubRelStr of MonMaps L,L st
for f being Function of L,L holds
( f is Element of b1 iff f is closure )
proof end;
correctness
uniqueness
for b1, b2 being non empty strict full SubRelStr of MonMaps L,L st ( for f being Function of L,L holds
( f is Element of b1 iff f is closure ) ) & ( for f being Function of L,L holds
( f is Element of b2 iff f is closure ) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def2 defines ClOpers WAYBEL10:def 2 :
for L being non empty reflexive RelStr
for b2 being non empty strict full SubRelStr of MonMaps L,L holds
( b2 = ClOpers L iff for f being Function of L,L holds
( f is Element of b2 iff f is closure ) );

theorem Th11: :: WAYBEL10:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty reflexive RelStr
for x being set holds
( x is Element of (ClOpers L) iff x is closure Function of L,L )
proof end;

theorem Th12: :: WAYBEL10:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th13: :: WAYBEL10:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th14: :: WAYBEL10:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th15: :: WAYBEL10:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

definition
let L be RelStr ;
func Sub L -> non empty strict RelStr means :Def3: :: WAYBEL10:def 3
( ( for x being set 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
ex b1 being non empty strict RelStr st
( ( for x being set holds
( x is Element of b1 iff x is strict SubRelStr of L ) ) & ( for a, b being Element of b1 holds
( a <= b iff ex R being RelStr st
( b = R & a is SubRelStr of R ) ) ) )
proof end;
correctness
uniqueness
for b1, b2 being non empty strict RelStr st ( for x being set holds
( x is Element of b1 iff x is strict SubRelStr of L ) ) & ( for a, b being Element of b1 holds
( a <= b iff ex R being RelStr st
( b = R & a is SubRelStr of R ) ) ) & ( for x being set holds
( x is Element of b2 iff x is strict SubRelStr of L ) ) & ( for a, b being Element of b2 holds
( a <= b iff ex R being RelStr st
( b = R & a is SubRelStr of R ) ) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def3 defines Sub WAYBEL10:def 3 :
for L being RelStr
for b2 being non empty strict RelStr holds
( b2 = Sub L iff ( ( for x being set holds
( x is Element of b2 iff x is strict SubRelStr of L ) ) & ( for a, b being Element of b2 holds
( a <= b iff ex R being RelStr st
( b = R & a is SubRelStr of R ) ) ) ) );

theorem Th16: :: WAYBEL10:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

registration
let L be RelStr ;
cluster Sub L -> non empty strict reflexive transitive antisymmetric ;
coherence
( Sub L is reflexive & Sub L is antisymmetric & Sub L is transitive )
proof end;
end;

registration
let L be RelStr ;
cluster Sub L -> non empty strict reflexive transitive antisymmetric complete ;
coherence
Sub L is complete
proof end;
end;

registration
let L be complete LATTICE;
cluster infs-inheriting -> non empty SubRelStr of L;
coherence
for b1 being SubRelStr of L st b1 is closure holds
not b1 is empty
proof end;
cluster sups-inheriting -> non empty SubRelStr of L;
coherence
for b1 being SubRelStr of L st b1 is sups-inheriting holds
not b1 is empty
proof end;
end;

definition
let L be RelStr ;
mode System of L is full SubRelStr of L;
end;

notation
let L be non empty RelStr ;
let S be System of L;
synonym closure S for infs-inheriting S;
end;

registration
let L be non empty RelStr ;
cluster subrelstr ([#] L) -> infs-inheriting sups-inheriting ;
coherence
( subrelstr ([#] L) is closure & subrelstr ([#] L) is sups-inheriting )
proof end;
end;

definition
let L be non empty RelStr ;
func ClosureSystems L -> non empty strict full SubRelStr of Sub L means :Def4: :: WAYBEL10:def 4
for R being strict SubRelStr of L holds
( R is Element of it iff ( R is closure & R is full ) );
existence
ex b1 being non empty strict full SubRelStr of Sub L st
for R being strict SubRelStr of L holds
( R is Element of b1 iff ( R is closure & R is full ) )
proof end;
correctness
uniqueness
for b1, b2 being non empty strict full SubRelStr of Sub L st ( for R being strict SubRelStr of L holds
( R is Element of b1 iff ( R is closure & R is full ) ) ) & ( for R being strict SubRelStr of L holds
( R is Element of b2 iff ( R is closure & R is full ) ) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def4 defines ClosureSystems WAYBEL10:def 4 :
for L being non empty RelStr
for b2 being non empty strict full SubRelStr of Sub L holds
( b2 = ClosureSystems L iff for R being strict SubRelStr of L holds
( R is Element of b2 iff ( R is closure & R is full ) ) );

theorem Th17: :: WAYBEL10:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty RelStr
for x being set holds
( x is Element of (ClosureSystems L) iff x is strict closure System of L )
proof end;

theorem Th18: :: WAYBEL10:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

registration
let L be non empty Poset;
let h be closure Function of L,L;
cluster Image h -> infs-inheriting ;
coherence
Image h is closure
by WAYBEL_1:56;
end;

definition
let L be non empty Poset;
func ClImageMap L -> Function of (ClOpers L),((ClosureSystems L) opp ) means :Def5: :: WAYBEL10:def 5
for c being closure Function of L,L holds it . c = Image c;
existence
ex b1 being Function of (ClOpers L),((ClosureSystems L) opp ) st
for c being closure Function of L,L holds b1 . c = Image c
proof end;
correctness
uniqueness
for b1, b2 being Function of (ClOpers L),((ClosureSystems L) opp ) st ( for c being closure Function of L,L holds b1 . c = Image c ) & ( for c being closure Function of L,L holds b2 . c = Image c ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def5 defines ClImageMap WAYBEL10:def 5 :
for L being non empty Poset
for b2 being Function of (ClOpers L),((ClosureSystems L) opp ) holds
( b2 = ClImageMap L iff for c being closure Function of L,L holds b2 . c = Image c );

definition
let L be non empty RelStr ;
let S be SubRelStr of L;
func closure_op S -> Function of L,L means :Def6: :: WAYBEL10:def 6
for x being Element of L holds it . x = "/\" ((uparrow x) /\ the carrier of S),L;
existence
ex b1 being Function of L,L st
for x being Element of L holds b1 . x = "/\" ((uparrow x) /\ the carrier of S),L
proof end;
uniqueness
for b1, b2 being Function of L,L st ( for x being Element of L holds b1 . x = "/\" ((uparrow x) /\ the carrier of S),L ) & ( for x being Element of L holds b2 . x = "/\" ((uparrow x) /\ the carrier of S),L ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines closure_op WAYBEL10:def 6 :
for L being non empty RelStr
for S being SubRelStr of L
for b3 being Function of L,L holds
( b3 = closure_op S iff for x being Element of L holds b3 . x = "/\" ((uparrow x) /\ the carrier of S),L );

registration
let L be complete LATTICE;
let S be closure System of L;
cluster closure_op S -> idempotent monotone closure ;
coherence
closure_op S is closure
proof end;
end;

theorem Th19: :: WAYBEL10:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 #)
proof end;

theorem Th20: :: WAYBEL10:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being complete LATTICE
for c being closure Function of L,L holds closure_op (Image c) = c
proof end;

registration
let L be complete LATTICE;
cluster ClImageMap L -> V5 ;
coherence
ClImageMap L is one-to-one
proof end;
end;

theorem Th21: :: WAYBEL10:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being complete LATTICE holds (ClImageMap L) " is Function of ((ClosureSystems L) opp ),(ClOpers L)
proof end;

theorem Th22: :: WAYBEL10:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being complete LATTICE
for S being strict closure System of L holds ((ClImageMap L) " ) . S = closure_op S
proof end;

registration
let L be complete LATTICE;
cluster ClImageMap L -> V5 isomorphic ;
correctness
coherence
ClImageMap L is isomorphic
;
proof end;
end;

theorem :: WAYBEL10:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being complete LATTICE holds ClOpers L,(ClosureSystems L) opp are_isomorphic
proof end;

theorem Th24: :: WAYBEL10:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

theorem Th25: :: WAYBEL10:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: WAYBEL10:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

registration
let L be complete LATTICE;
let S be closure directed-sups-inheriting System of L;
cluster closure_op S -> idempotent monotone directed-sups-preserving closure ;
coherence
closure_op S is directed-sups-preserving
by Th25;
end;

registration
let L be complete LATTICE;
let h be directed-sups-preserving closure Function of L,L;
cluster Image h -> infs-inheriting directed-sups-inheriting ;
coherence
Image h is directed-sups-inheriting
proof end;
end;

definition
let L be non empty reflexive RelStr ;
func DsupClOpers L -> non empty strict full SubRelStr of ClOpers L means :Def7: :: WAYBEL10:def 7
for f being closure Function of L,L holds
( f is Element of it iff f is directed-sups-preserving );
existence
ex b1 being non empty strict full SubRelStr of ClOpers L st
for f being closure Function of L,L holds
( f is Element of b1 iff f is directed-sups-preserving )
proof end;
correctness
uniqueness
for b1, b2 being non empty strict full SubRelStr of ClOpers L st ( for f being closure Function of L,L holds
( f is Element of b1 iff f is directed-sups-preserving ) ) & ( for f being closure Function of L,L holds
( f is Element of b2 iff f is directed-sups-preserving ) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def7 defines DsupClOpers WAYBEL10:def 7 :
for L being non empty reflexive RelStr
for b2 being non empty strict full SubRelStr of ClOpers L holds
( b2 = DsupClOpers L iff for f being closure Function of L,L holds
( f is Element of b2 iff f is directed-sups-preserving ) );

theorem Th27: :: WAYBEL10:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

definition
let L be non empty RelStr ;
func Subalgebras L -> non empty strict full SubRelStr of ClosureSystems L means :Def8: :: WAYBEL10:def 8
for R being strict closure System of L holds
( R is Element of it iff R is directed-sups-inheriting );
existence
ex b1 being non empty strict full SubRelStr of ClosureSystems L st
for R being strict closure System of L holds
( R is Element of b1 iff R is directed-sups-inheriting )
proof end;
correctness
uniqueness
for b1, b2 being non empty strict full SubRelStr of ClosureSystems L st ( for R being strict closure System of L holds
( R is Element of b1 iff R is directed-sups-inheriting ) ) & ( for R being strict closure System of L holds
( R is Element of b2 iff R is directed-sups-inheriting ) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def8 defines Subalgebras WAYBEL10:def 8 :
for L being non empty RelStr
for b2 being non empty strict full SubRelStr of ClosureSystems L holds
( b2 = Subalgebras L iff for R being strict closure System of L holds
( R is Element of b2 iff R is directed-sups-inheriting ) );

theorem Th28: :: WAYBEL10:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty RelStr
for x being set holds
( x is Element of (Subalgebras L) iff x is strict closure directed-sups-inheriting System of L )
proof end;

theorem Th29: :: WAYBEL10:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being complete LATTICE holds Image ((ClImageMap L) | (DsupClOpers L)) = (Subalgebras L) opp
proof end;

registration
let L be complete LATTICE;
cluster corestr ((ClImageMap L) | (DsupClOpers L)) -> monotone isomorphic ;
coherence
corestr ((ClImageMap L) | (DsupClOpers L)) is isomorphic
proof end;
end;

theorem :: WAYBEL10:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being complete LATTICE holds DsupClOpers L,(Subalgebras L) opp are_isomorphic
proof end;