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

notation
let L be RelStr ;
synonym L opp for L ~ ;
end;

theorem Th1: :: YELLOW_7:1  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 x, y being Element of (L opp ) holds
( x <= y iff ~ x >= ~ y )
proof end;

theorem Th2: :: YELLOW_7:2  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 x being Element of L
for y being Element of (L opp ) holds
( ( x <= ~ y implies x ~ >= y ) & ( x ~ >= y implies x <= ~ y ) & ( x >= ~ y implies x ~ <= y ) & ( x ~ <= y implies x >= ~ y ) )
proof end;

theorem :: YELLOW_7:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being RelStr holds
( L is empty iff L opp is empty )
proof end;

theorem Th4: :: YELLOW_7:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being RelStr holds
( L is reflexive iff L opp is reflexive )
proof end;

theorem Th5: :: YELLOW_7: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 holds
( L is antisymmetric iff L opp is antisymmetric )
proof end;

theorem Th6: :: YELLOW_7:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being RelStr holds
( L is transitive iff L opp is transitive )
proof end;

theorem Th7: :: YELLOW_7:7  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 holds
( L is connected iff L opp is connected )
proof end;

registration
let L be reflexive RelStr ;
cluster L opp -> reflexive ;
coherence
L opp is reflexive
by Th4;
end;

registration
let L be transitive RelStr ;
cluster L opp -> transitive ;
coherence
L opp is transitive
by Th6;
end;

registration
let L be antisymmetric RelStr ;
cluster L opp -> antisymmetric ;
coherence
L opp is antisymmetric
by Th5;
end;

registration
let L be non empty connected RelStr ;
cluster L opp -> connected ;
coherence
L opp is connected
by Th7;
end;

theorem Th8: :: YELLOW_7:8  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 x being Element of L
for X being set holds
( ( x is_<=_than X implies x ~ is_>=_than X ) & ( x ~ is_>=_than X implies x is_<=_than X ) & ( x is_>=_than X implies x ~ is_<=_than X ) & ( x ~ is_<=_than X implies x is_>=_than X ) )
proof end;

theorem Th9: :: YELLOW_7:9  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 x being Element of (L opp )
for X being set holds
( ( x is_<=_than X implies ~ x is_>=_than X ) & ( ~ x is_>=_than X implies x is_<=_than X ) & ( x is_>=_than X implies ~ x is_<=_than X ) & ( ~ x is_<=_than X implies x is_>=_than X ) )
proof end;

theorem Th10: :: YELLOW_7:10  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 X being set holds
( ex_sup_of X,L iff ex_inf_of X,L opp )
proof end;

theorem Th11: :: YELLOW_7:11  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 X being set holds
( ex_sup_of X,L opp iff ex_inf_of X,L )
proof end;

theorem Th12: :: YELLOW_7:12  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 st ( ex_sup_of X,L or ex_inf_of X,L opp ) holds
"\/" X,L = "/\" X,(L opp )
proof end;

theorem Th13: :: YELLOW_7:13  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 st ( ex_inf_of X,L or ex_sup_of X,L opp ) holds
"/\" X,L = "\/" X,(L opp )
proof end;

theorem Th14: :: YELLOW_7:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being RelStr st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) & L1 is with_infima holds
L2 is with_infima
proof end;

theorem :: YELLOW_7:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being RelStr st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) & L1 is with_suprema holds
L2 is with_suprema
proof end;

theorem Th16: :: YELLOW_7:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being RelStr holds
( L is with_infima iff L opp is with_suprema )
proof end;

theorem Th17: :: YELLOW_7: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 holds
( L is complete iff L opp is complete )
proof end;

registration
let L be with_infima RelStr ;
cluster L opp -> with_suprema ;
coherence
L opp is with_suprema
by Th16;
end;

registration
let L be with_suprema RelStr ;
cluster L opp -> with_infima ;
coherence
L opp is with_infima
by LATTICE3:10;
end;

registration
let L be non empty complete RelStr ;
cluster L opp -> with_suprema with_infima complete ;
coherence
L opp is complete
by Th17;
end;

theorem :: YELLOW_7: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 X being Subset of L
for Y being Subset of (L opp ) st X = Y holds
( fininfs X = finsups Y & finsups X = fininfs Y )
proof end;

theorem Th19: :: YELLOW_7:19  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 X being Subset of L
for Y being Subset of (L opp ) st X = Y holds
( downarrow X = uparrow Y & uparrow X = downarrow Y )
proof end;

theorem :: YELLOW_7:20  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 Element of L
for y being Element of (L opp ) st x = y holds
( downarrow x = uparrow y & uparrow x = downarrow y ) by Th19;

theorem Th21: :: YELLOW_7:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being with_infima Poset
for x, y being Element of L holds x "/\" y = (x ~ ) "\/" (y ~ )
proof end;

theorem Th22: :: YELLOW_7:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being with_infima Poset
for x, y being Element of (L opp ) holds (~ x) "/\" (~ y) = x "\/" y
proof end;

theorem Th23: :: YELLOW_7:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being with_suprema Poset
for x, y being Element of L holds x "\/" y = (x ~ ) "/\" (y ~ )
proof end;

theorem Th24: :: YELLOW_7:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being with_suprema Poset
for x, y being Element of (L opp ) holds (~ x) "\/" (~ y) = x "/\" y
proof end;

theorem Th25: :: YELLOW_7:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being LATTICE holds
( L is distributive iff L opp is distributive )
proof end;

registration
let L be distributive LATTICE;
cluster L opp -> with_suprema with_infima distributive ;
coherence
L opp is distributive
by Th25;
end;

theorem Th26: :: YELLOW_7:26  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 x being set holds
( x is directed Subset of L iff x is filtered Subset of (L opp ) )
proof end;

theorem :: YELLOW_7:27  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 x being set holds
( x is directed Subset of (L opp ) iff x is filtered Subset of L )
proof end;

theorem Th28: :: YELLOW_7:28  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 x being set holds
( x is lower Subset of L iff x is upper Subset of (L opp ) )
proof end;

theorem :: YELLOW_7:29  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 x being set holds
( x is lower Subset of (L opp ) iff x is upper Subset of L )
proof end;

theorem Th30: :: YELLOW_7:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being RelStr holds
( L is lower-bounded iff L opp is upper-bounded )
proof end;

theorem Th31: :: YELLOW_7:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being RelStr holds
( L opp is lower-bounded iff L is upper-bounded )
proof end;

theorem :: YELLOW_7:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being RelStr holds
( L is bounded iff L opp is bounded )
proof end;

theorem Th33: :: YELLOW_7:33  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 antisymmetric lower-bounded RelStr holds
( (Bottom L) ~ = Top (L opp ) & ~ (Top (L opp )) = Bottom L )
proof end;

theorem Th34: :: YELLOW_7:34  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 antisymmetric upper-bounded RelStr holds
( (Top L) ~ = Bottom (L opp ) & ~ (Bottom (L opp )) = Top L )
proof end;

theorem Th35: :: YELLOW_7:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being bounded LATTICE
for x, y being Element of L holds
( y is_a_complement_of x iff y ~ is_a_complement_of x ~ )
proof end;

theorem Th36: :: YELLOW_7:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being bounded LATTICE holds
( L is complemented iff L opp is complemented )
proof end;

registration
let L be lower-bounded RelStr ;
cluster L opp -> upper-bounded ;
coherence
L opp is upper-bounded
by Th30;
end;

registration
let L be upper-bounded RelStr ;
cluster L opp -> lower-bounded ;
coherence
L opp is lower-bounded
by Th31;
end;

registration
let L be bounded complemented LATTICE;
cluster L opp -> with_suprema with_infima lower-bounded upper-bounded complemented ;
coherence
L opp is complemented
by Th36;
end;

theorem :: YELLOW_7:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Boolean LATTICE
for x being Element of L holds 'not' (x ~ ) = 'not' x
proof end;

definition
let L be non empty RelStr ;
func ComplMap L -> Function of L,(L opp ) means :Def1: :: YELLOW_7:def 1
for x being Element of L holds it . x = 'not' x;
existence
ex b1 being Function of L,(L opp ) st
for x being Element of L holds b1 . x = 'not' x
proof end;
correctness
uniqueness
for b1, b2 being Function of L,(L opp ) st ( for x being Element of L holds b1 . x = 'not' x ) & ( for x being Element of L holds b2 . x = 'not' x ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def1 defines ComplMap YELLOW_7:def 1 :
for L being non empty RelStr
for b2 being Function of L,(L opp ) holds
( b2 = ComplMap L iff for x being Element of L holds b2 . x = 'not' x );

registration
let L be Boolean LATTICE;
cluster ComplMap L -> V6 ;
coherence
ComplMap L is one-to-one
proof end;
end;

registration
let L be Boolean LATTICE;
cluster ComplMap L -> V6 isomorphic ;
coherence
ComplMap L is isomorphic
proof end;
end;

theorem :: YELLOW_7:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Boolean LATTICE holds L,L opp are_isomorphic
proof end;

theorem :: YELLOW_7:39  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 f being set holds
( ( f is Function of S,T implies f is Function of (S opp ),T ) & ( f is Function of (S opp ),T implies f is Function of S,T ) & ( f is Function of S,T implies f is Function of S,(T opp ) ) & ( f is Function of S,(T opp ) implies f is Function of S,T ) & ( f is Function of S,T implies f is Function of (S opp ),(T opp ) ) & ( f is Function of (S opp ),(T opp ) implies f is Function of S,T ) ) ;

theorem :: YELLOW_7:40  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 f being Function of S,T
for g being Function of S,(T opp ) st f = g holds
( ( f is monotone implies g is antitone ) & ( g is antitone implies f is monotone ) & ( f is antitone implies g is monotone ) & ( g is monotone implies f is antitone ) )
proof end;

theorem :: YELLOW_7:41  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 f being Function of S,(T opp )
for g being Function of (S opp ),T st f = g holds
( ( f is monotone implies g is monotone ) & ( g is monotone implies f is monotone ) & ( f is antitone implies g is antitone ) & ( g is antitone implies f is antitone ) )
proof end;

theorem Th42: :: YELLOW_7:42  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 f being Function of S,T
for g being Function of (S opp ),(T opp ) st f = g holds
( ( f is monotone implies g is monotone ) & ( g is monotone implies f is monotone ) & ( f is antitone implies g is antitone ) & ( g is antitone implies f is antitone ) )
proof end;

theorem :: YELLOW_7:43  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 f being set holds
( ( f is Connection of S,T implies f is Connection of S ~ ,T ) & ( f is Connection of S ~ ,T implies f is Connection of S,T ) & ( f is Connection of S,T implies f is Connection of S,T ~ ) & ( f is Connection of S,T ~ implies f is Connection of S,T ) & ( f is Connection of S,T implies f is Connection of S ~ ,T ~ ) & ( f is Connection of S ~ ,T ~ implies f is Connection of S,T ) )
proof end;

theorem :: YELLOW_7:44  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 Poset
for f1 being Function of S,T
for g1 being Function of T,S
for f2 being Function of (S ~ ),(T ~ )
for g2 being Function of (T ~ ),(S ~ ) st f1 = f2 & g1 = g2 holds
( [f1,g1] is Galois iff [g2,f2] is Galois )
proof end;

theorem Th45: :: YELLOW_7:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for J being set
for D being non empty set
for K being ManySortedSet of J
for F being DoubleIndexedSet of K,D holds doms F = K
proof end;

definition
let J, D be non empty set ;
let K be V3 ManySortedSet of J;
let F be DoubleIndexedSet of K,D;
let j be Element of J;
let k be Element of K . j;
:: original: ..
redefine func F .. j,k -> Element of D;
coherence
F .. j,k is Element of D
proof end;
end;

theorem :: YELLOW_7:46  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 J being set
for K being ManySortedSet of J
for x being set holds
( x is DoubleIndexedSet of K,L iff x is DoubleIndexedSet of K,(L opp ) ) ;

theorem Th47: :: YELLOW_7:47  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 J being non empty set
for K being V3 ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Sup <= Inf
proof end;

theorem Th48: :: YELLOW_7:48  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
( L is completely-distributive iff for J being non empty set
for K being V3 ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Sup = Inf )
proof end;

theorem Th49: :: YELLOW_7:49  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 antisymmetric complete RelStr
for F being Function holds
( \\/ F,L = //\ F,(L opp ) & //\ F,L = \\/ F,(L opp ) )
proof end;

theorem Th50: :: YELLOW_7:50  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 antisymmetric complete RelStr
for F being Function-yielding Function holds
( \// F,L = /\\ F,(L opp ) & /\\ F,L = \// F,(L opp ) )
proof end;

registration
cluster non empty completely-distributive -> non empty complete RelStr ;
coherence
for b1 being non empty RelStr st b1 is completely-distributive holds
b1 is complete
by WAYBEL_5:def 3;
end;

registration
cluster non empty strict complete completely-distributive trivial RelStr ;
existence
ex b1 being non empty Poset st
( b1 is completely-distributive & b1 is trivial & b1 is strict )
proof end;
end;

theorem :: YELLOW_7:51  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 Poset holds
( L is completely-distributive iff L opp is completely-distributive )
proof end;