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

deffunc H1( LattStr ) -> set = the carrier of $1;

deffunc H2( LattStr ) -> M5([:the carrier of $1,the carrier of $1:],the carrier of $1) = the L_join of $1;

deffunc H3( LattStr ) -> M5([:the carrier of $1,the carrier of $1:],the carrier of $1) = the L_meet of $1;

theorem Th1: :: FILTER_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for F1, F2 being Filter of L holds F1 /\ F2 is Filter of L
proof end;

theorem :: FILTER_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for p, q being Element of L st <.p.) = <.q.) holds
p = q
proof end;

definition
let L be Lattice;
let F1, F2 be Filter of L;
:: original: /\
redefine func F1 /\ F2 -> Filter of L;
coherence
F1 /\ F2 is Filter of L
by Th1;
end;

definition
let D be non empty set ;
let R be Relation;
mode UnOp of D,R -> UnOp of D means :Def1: :: FILTER_1:def 1
for x, y being Element of D st [x,y] in R holds
[(it . x),(it . y)] in R;
existence
ex b1 being UnOp of D st
for x, y being Element of D st [x,y] in R holds
[(b1 . x),(b1 . y)] in R
proof end;
mode BinOp of D,R -> BinOp of D means :Def2: :: FILTER_1:def 2
for x1, y1, x2, y2 being Element of D st [x1,y1] in R & [x2,y2] in R holds
[(it . x1,x2),(it . y1,y2)] in R;
existence
ex b1 being BinOp of D st
for x1, y1, x2, y2 being Element of D st [x1,y1] in R & [x2,y2] in R holds
[(b1 . x1,x2),(b1 . y1,y2)] in R
proof end;
end;

:: deftheorem Def1 defines UnOp FILTER_1:def 1 :
for D being non empty set
for R being Relation
for b3 being UnOp of D holds
( b3 is UnOp of D,R iff for x, y being Element of D st [x,y] in R holds
[(b3 . x),(b3 . y)] in R );

:: deftheorem Def2 defines BinOp FILTER_1:def 2 :
for D being non empty set
for R being Relation
for b3 being BinOp of D holds
( b3 is BinOp of D,R iff for x1, y1, x2, y2 being Element of D st [x1,y1] in R & [x2,y2] in R holds
[(b3 . x1,x2),(b3 . y1,y2)] in R );

definition
let D be non empty set ;
let R be Equivalence_Relation of D;
mode UnOp of R is UnOp of D,R;
mode BinOp of R is BinOp of D,R;
end;

registration
let D be non empty set ;
let R be Equivalence_Relation of D;
cluster Class R -> non empty ;
coherence
not Class R is empty
proof end;
end;

definition
let D be non empty set ;
let R be Equivalence_Relation of D;
let d be Element of D;
:: original: Class
redefine func Class R,d -> Element of Class R;
coherence
Class R,d is Element of Class R
by EQREL_1:def 5;
end;

definition
let D be non empty set ;
let R be Equivalence_Relation of D;
let u be UnOp of D;
assume A1: u is UnOp of D,R ;
func u /\/ R -> UnOp of Class R means :: FILTER_1:def 3
for x, y being set st x in Class R & y in x holds
it . x = Class R,(u . y);
existence
ex b1 being UnOp of Class R st
for x, y being set st x in Class R & y in x holds
b1 . x = Class R,(u . y)
proof end;
uniqueness
for b1, b2 being UnOp of Class R st ( for x, y being set st x in Class R & y in x holds
b1 . x = Class R,(u . y) ) & ( for x, y being set st x in Class R & y in x holds
b2 . x = Class R,(u . y) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines /\/ FILTER_1:def 3 :
for D being non empty set
for R being Equivalence_Relation of D
for u being UnOp of D st u is UnOp of D,R holds
for b4 being UnOp of Class R holds
( b4 = u /\/ R iff for x, y being set st x in Class R & y in x holds
b4 . x = Class R,(u . y) );

definition
let D be non empty set ;
let R be Equivalence_Relation of D;
let b be BinOp of D;
assume A1: b is BinOp of D,R ;
func b /\/ R -> BinOp of Class R means :Def4: :: FILTER_1:def 4
for x, y, x1, y1 being set st x in Class R & y in Class R & x1 in x & y1 in y holds
it . x,y = Class R,(b . x1,y1);
existence
ex b1 being BinOp of Class R st
for x, y, x1, y1 being set st x in Class R & y in Class R & x1 in x & y1 in y holds
b1 . x,y = Class R,(b . x1,y1)
proof end;
uniqueness
for b1, b2 being BinOp of Class R st ( for x, y, x1, y1 being set st x in Class R & y in Class R & x1 in x & y1 in y holds
b1 . x,y = Class R,(b . x1,y1) ) & ( for x, y, x1, y1 being set st x in Class R & y in Class R & x1 in x & y1 in y holds
b2 . x,y = Class R,(b . x1,y1) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines /\/ FILTER_1:def 4 :
for D being non empty set
for R being Equivalence_Relation of D
for b being BinOp of D st b is BinOp of D,R holds
for b4 being BinOp of Class R holds
( b4 = b /\/ R iff for x, y, x1, y1 being set st x in Class R & y in Class R & x1 in x & y1 in y holds
b4 . x,y = Class R,(b . x1,y1) );

theorem Th3: :: FILTER_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for RD being Equivalence_Relation of D
for a, b being Element of D
for F being BinOp of D,RD holds (F /\/ RD) . (Class RD,a),(Class RD,b) = Class RD,(F . a,b)
proof end;

scheme :: FILTER_1:sch 1
SchAux1{ F1() -> non empty set , F2() -> Equivalence_Relation of F1(), P1[ set ] } :
for x being Element of Class F2() holds P1[x]
provided
A1: for x being Element of F1() holds P1[ Class F2(),x]
proof end;

scheme :: FILTER_1:sch 2
SchAux2{ F1() -> non empty set , F2() -> Equivalence_Relation of F1(), P1[ set , set ] } :
for x, y being Element of Class F2() holds P1[x,y]
provided
A1: for x, y being Element of F1() holds P1[ Class F2(),x, Class F2(),y]
proof end;

scheme :: FILTER_1:sch 3
SchAux3{ F1() -> non empty set , F2() -> Equivalence_Relation of F1(), P1[ set , set , set ] } :
for x, y, z being Element of Class F2() holds P1[x,y,z]
provided
A1: for x, y, z being Element of F1() holds P1[ Class F2(),x, Class F2(),y, Class F2(),z]
proof end;

theorem Th4: :: FILTER_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for RD being Equivalence_Relation of D
for F being BinOp of D,RD st F is commutative holds
F /\/ RD is commutative
proof end;

theorem Th5: :: FILTER_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for RD being Equivalence_Relation of D
for F being BinOp of D,RD st F is associative holds
F /\/ RD is associative
proof end;

theorem Th6: :: FILTER_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for RD being Equivalence_Relation of D
for d being Element of D
for F being BinOp of D,RD st d is_a_left_unity_wrt F holds
Class RD,d is_a_left_unity_wrt F /\/ RD
proof end;

theorem Th7: :: FILTER_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for RD being Equivalence_Relation of D
for d being Element of D
for F being BinOp of D,RD st d is_a_right_unity_wrt F holds
Class RD,d is_a_right_unity_wrt F /\/ RD
proof end;

theorem :: FILTER_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for RD being Equivalence_Relation of D
for d being Element of D
for F being BinOp of D,RD st d is_a_unity_wrt F holds
Class RD,d is_a_unity_wrt F /\/ RD
proof end;

theorem Th9: :: FILTER_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for RD being Equivalence_Relation of D
for F, G being BinOp of D,RD st F is_left_distributive_wrt G holds
F /\/ RD is_left_distributive_wrt G /\/ RD
proof end;

theorem Th10: :: FILTER_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for RD being Equivalence_Relation of D
for F, G being BinOp of D,RD st F is_right_distributive_wrt G holds
F /\/ RD is_right_distributive_wrt G /\/ RD
proof end;

theorem :: FILTER_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for RD being Equivalence_Relation of D
for F, G being BinOp of D,RD st F is_distributive_wrt G holds
F /\/ RD is_distributive_wrt G /\/ RD
proof end;

theorem Th12: :: FILTER_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for RD being Equivalence_Relation of D
for F, G being BinOp of D,RD st F absorbs G holds
F /\/ RD absorbs G /\/ RD
proof end;

theorem Th13: :: FILTER_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being I_Lattice
for FI being Filter of I holds the L_join of I is BinOp of the carrier of I, equivalence_wrt FI
proof end;

theorem Th14: :: FILTER_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being I_Lattice
for FI being Filter of I holds the L_meet of I is BinOp of the carrier of I, equivalence_wrt FI
proof end;

definition
let L be Lattice;
let F be Filter of L;
assume A1: L is I_Lattice ;
func L /\/ F -> strict Lattice means :Def5: :: FILTER_1:def 5
for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds
it = LattStr(# (Class R),(the L_join of L /\/ R),(the L_meet of L /\/ R) #);
existence
ex b1 being strict Lattice st
for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds
b1 = LattStr(# (Class R),(the L_join of L /\/ R),(the L_meet of L /\/ R) #)
proof end;
uniqueness
for b1, b2 being strict Lattice st ( for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds
b1 = LattStr(# (Class R),(the L_join of L /\/ R),(the L_meet of L /\/ R) #) ) & ( for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds
b2 = LattStr(# (Class R),(the L_join of L /\/ R),(the L_meet of L /\/ R) #) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines /\/ FILTER_1:def 5 :
for L being Lattice
for F being Filter of L st L is I_Lattice holds
for b3 being strict Lattice holds
( b3 = L /\/ F iff for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds
b3 = LattStr(# (Class R),(the L_join of L /\/ R),(the L_meet of L /\/ R) #) );

definition
let L be Lattice;
let F be Filter of L;
let a be Element of L;
assume A1: L is I_Lattice ;
func a /\/ F -> Element of (L /\/ F) means :Def6: :: FILTER_1:def 6
for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds
it = Class R,a;
existence
ex b1 being Element of (L /\/ F) st
for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds
b1 = Class R,a
proof end;
uniqueness
for b1, b2 being Element of (L /\/ F) st ( for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds
b1 = Class R,a ) & ( for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds
b2 = Class R,a ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines /\/ FILTER_1:def 6 :
for L being Lattice
for F being Filter of L
for a being Element of L st L is I_Lattice holds
for b4 being Element of (L /\/ F) holds
( b4 = a /\/ F iff for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds
b4 = Class R,a );

theorem Th15: :: FILTER_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being I_Lattice
for FI being Filter of I
for i, j being Element of I holds
( (i /\/ FI) "\/" (j /\/ FI) = (i "\/" j) /\/ FI & (i /\/ FI) "/\" (j /\/ FI) = (i "/\" j) /\/ FI )
proof end;

theorem Th16: :: FILTER_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being I_Lattice
for FI being Filter of I
for i, j being Element of I holds
( i /\/ FI [= j /\/ FI iff i => j in FI )
proof end;

theorem Th17: :: FILTER_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being I_Lattice
for i, j, k being Element of I holds (i "/\" j) => k = i => (j => k)
proof end;

theorem Th18: :: FILTER_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being I_Lattice
for FI being Filter of I st I is lower-bounded holds
( I /\/ FI is 0_Lattice & Bottom (I /\/ FI) = (Bottom I) /\/ FI )
proof end;

theorem Th19: :: FILTER_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being I_Lattice
for FI being Filter of I holds
( I /\/ FI is 1_Lattice & Top (I /\/ FI) = (Top I) /\/ FI )
proof end;

theorem Th20: :: FILTER_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being I_Lattice
for FI being Filter of I holds I /\/ FI is implicative
proof end;

theorem :: FILTER_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B being B_Lattice
for FB being Filter of B holds B /\/ FB is B_Lattice
proof end;

definition
let D1, D2 be set ;
let f1 be BinOp of D1;
let f2 be BinOp of D2;
:: original: |:
redefine func |:f1,f2:| -> BinOp of [:D1,D2:];
coherence
|:f1,f2:| is BinOp of [:D1,D2:]
proof end;
end;

theorem Th22: :: FILTER_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D1, D2 being non empty set
for a1, b1 being Element of D1
for a2, b2 being Element of D2
for f1 being BinOp of D1
for f2 being BinOp of D2 holds |:f1,f2:| . [a1,a2],[b1,b2] = [(f1 . a1,b1),(f2 . a2,b2)]
proof end;

scheme :: FILTER_1:sch 4
AuxCart1{ F1() -> non empty set , F2() -> non empty set , P1[ set ] } :
for d being Element of [:F1(),F2():] holds P1[d]
provided
A1: for d1 being Element of F1()
for d2 being Element of F2() holds P1[[d1,d2]]
proof end;

scheme :: FILTER_1:sch 5
AuxCart2{ F1() -> non empty set , F2() -> non empty set , P1[ set , set ] } :
for d, d' being Element of [:F1(),F2():] holds P1[d,d']
provided
A1: for d1, d1' being Element of F1()
for d2, d2' being Element of F2() holds P1[[d1,d2],[d1',d2']]
proof end;

scheme :: FILTER_1:sch 6
AuxCart3{ F1() -> non empty set , F2() -> non empty set , P1[ set , set , set ] } :
for a, b, c being Element of [:F1(),F2():] holds P1[a,b,c]
provided
A1: for a1, b1, c1 being Element of F1()
for a2, b2, c2 being Element of F2() holds P1[[a1,a2],[b1,b2],[c1,c2]]
proof end;

theorem Th23: :: FILTER_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D1, D2 being non empty set
for f1 being BinOp of D1
for f2 being BinOp of D2 holds
( ( f1 is commutative & f2 is commutative ) iff |:f1,f2:| is commutative )
proof end;

theorem Th24: :: FILTER_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D1, D2 being non empty set
for f1 being BinOp of D1
for f2 being BinOp of D2 holds
( ( f1 is associative & f2 is associative ) iff |:f1,f2:| is associative )
proof end;

theorem Th25: :: FILTER_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D1, D2 being non empty set
for a1 being Element of D1
for a2 being Element of D2
for f1 being BinOp of D1
for f2 being BinOp of D2 holds
( ( a1 is_a_left_unity_wrt f1 & a2 is_a_left_unity_wrt f2 ) iff [a1,a2] is_a_left_unity_wrt |:f1,f2:| )
proof end;

theorem Th26: :: FILTER_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D1, D2 being non empty set
for a1 being Element of D1
for a2 being Element of D2
for f1 being BinOp of D1
for f2 being BinOp of D2 holds
( ( a1 is_a_right_unity_wrt f1 & a2 is_a_right_unity_wrt f2 ) iff [a1,a2] is_a_right_unity_wrt |:f1,f2:| )
proof end;

theorem :: FILTER_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D1, D2 being non empty set
for a1 being Element of D1
for a2 being Element of D2
for f1 being BinOp of D1
for f2 being BinOp of D2 holds
( ( a1 is_a_unity_wrt f1 & a2 is_a_unity_wrt f2 ) iff [a1,a2] is_a_unity_wrt |:f1,f2:| )
proof end;

theorem Th28: :: FILTER_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D1, D2 being non empty set
for f1, g1 being BinOp of D1
for f2, g2 being BinOp of D2 holds
( ( f1 is_left_distributive_wrt g1 & f2 is_left_distributive_wrt g2 ) iff |:f1,f2:| is_left_distributive_wrt |:g1,g2:| )
proof end;

theorem Th29: :: FILTER_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D1, D2 being non empty set
for f1, g1 being BinOp of D1
for f2, g2 being BinOp of D2 holds
( ( f1 is_right_distributive_wrt g1 & f2 is_right_distributive_wrt g2 ) iff |:f1,f2:| is_right_distributive_wrt |:g1,g2:| )
proof end;

theorem Th30: :: FILTER_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D1, D2 being non empty set
for f1, g1 being BinOp of D1
for f2, g2 being BinOp of D2 holds
( ( f1 is_distributive_wrt g1 & f2 is_distributive_wrt g2 ) iff |:f1,f2:| is_distributive_wrt |:g1,g2:| )
proof end;

theorem Th31: :: FILTER_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D1, D2 being non empty set
for f1, g1 being BinOp of D1
for f2, g2 being BinOp of D2 holds
( ( f1 absorbs g1 & f2 absorbs g2 ) iff |:f1,f2:| absorbs |:g1,g2:| )
proof end;

definition
let L1, L2 be non empty LattStr ;
func [:L1,L2:] -> strict LattStr equals :: FILTER_1:def 7
LattStr(# [:the carrier of L1,the carrier of L2:],|:the L_join of L1,the L_join of L2:|,|:the L_meet of L1,the L_meet of L2:| #);
correctness
coherence
LattStr(# [:the carrier of L1,the carrier of L2:],|:the L_join of L1,the L_join of L2:|,|:the L_meet of L1,the L_meet of L2:| #) is strict LattStr
;
;
end;

:: deftheorem defines [: FILTER_1:def 7 :
for L1, L2 being non empty LattStr holds [:L1,L2:] = LattStr(# [:the carrier of L1,the carrier of L2:],|:the L_join of L1,the L_join of L2:|,|:the L_meet of L1,the L_meet of L2:| #);

registration
let L1, L2 be non empty LattStr ;
cluster [:L1,L2:] -> non empty strict ;
coherence
not [:L1,L2:] is empty
;
end;

definition
let L be Lattice;
func LattRel L -> Relation equals :: FILTER_1:def 8
{ [p,q] where p, q is Element of L : p [= q } ;
coherence
{ [p,q] where p, q is Element of L : p [= q } is Relation
proof end;
end;

:: deftheorem defines LattRel FILTER_1:def 8 :
for L being Lattice holds LattRel L = { [p,q] where p, q is Element of L : p [= q } ;

theorem Th32: :: FILTER_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for p, q being Element of L holds
( [p,q] in LattRel L iff p [= q )
proof end;

theorem Th33: :: FILTER_1:33  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
( dom (LattRel L) = the carrier of L & rng (LattRel L) = the carrier of L & field (LattRel L) = the carrier of L )
proof end;

definition
let L1, L2 be Lattice;
pred L1,L2 are_isomorphic means :: FILTER_1:def 9
LattRel L1, LattRel L2 are_isomorphic ;
reflexivity
for L1 being Lattice holds LattRel L1, LattRel L1 are_isomorphic
by WELLORD1:48;
symmetry
for L1, L2 being Lattice st LattRel L1, LattRel L2 are_isomorphic holds
LattRel L2, LattRel L1 are_isomorphic
by WELLORD1:50;
end;

:: deftheorem defines are_isomorphic FILTER_1:def 9 :
for L1, L2 being Lattice holds
( L1,L2 are_isomorphic iff LattRel L1, LattRel L2 are_isomorphic );

registration
let L1, L2 be Lattice;
cluster [:L1,L2:] -> non empty strict Lattice-like ;
coherence
[:L1,L2:] is Lattice-like
proof end;
end;

theorem :: FILTER_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2, L3 being Lattice st L1,L2 are_isomorphic & L2,L3 are_isomorphic holds
L1,L3 are_isomorphic
proof end;

theorem :: FILTER_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being non empty LattStr st [:L1,L2:] is Lattice holds
( L1 is Lattice & L2 is Lattice )
proof end;

definition
let L1, L2 be Lattice;
let a be Element of L1;
let b be Element of L2;
:: original: [
redefine func [a,b] -> Element of [:L1,L2:];
coherence
[a,b] is Element of [:L1,L2:]
proof end;
end;

theorem Th36: :: FILTER_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being Lattice
for p1, q1 being Element of L1
for p2, q2 being Element of L2 holds
( [p1,p2] "\/" [q1,q2] = [(p1 "\/" q1),(p2 "\/" q2)] & [p1,p2] "/\" [q1,q2] = [(p1 "/\" q1),(p2 "/\" q2)] ) by Th22;

theorem Th37: :: FILTER_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being Lattice
for p1, q1 being Element of L1
for p2, q2 being Element of L2 holds
( [p1,p2] [= [q1,q2] iff ( p1 [= q1 & p2 [= q2 ) )
proof end;

theorem :: FILTER_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being Lattice holds
( ( L1 is modular & L2 is modular ) iff [:L1,L2:] is modular )
proof end;

theorem Th39: :: FILTER_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being Lattice holds
( ( L1 is D_Lattice & L2 is D_Lattice ) iff [:L1,L2:] is D_Lattice )
proof end;

theorem Th40: :: FILTER_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being Lattice holds
( ( L1 is lower-bounded & L2 is lower-bounded ) iff [:L1,L2:] is lower-bounded )
proof end;

theorem Th41: :: FILTER_1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being Lattice holds
( ( L1 is upper-bounded & L2 is upper-bounded ) iff [:L1,L2:] is upper-bounded )
proof end;

theorem Th42: :: FILTER_1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being Lattice holds
( ( L1 is bounded & L2 is bounded ) iff [:L1,L2:] is bounded )
proof end;

theorem Th43: :: FILTER_1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being Lattice st L1 is 0_Lattice & L2 is 0_Lattice holds
Bottom [:L1,L2:] = [(Bottom L1),(Bottom L2)]
proof end;

theorem Th44: :: FILTER_1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being Lattice st L1 is 1_Lattice & L2 is 1_Lattice holds
Top [:L1,L2:] = [(Top L1),(Top L2)]
proof end;

theorem Th45: :: FILTER_1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being Lattice
for p1, q1 being Element of L1
for p2, q2 being Element of L2 st L1 is 01_Lattice & L2 is 01_Lattice holds
( ( p1 is_a_complement_of q1 & p2 is_a_complement_of q2 ) iff [p1,p2] is_a_complement_of [q1,q2] )
proof end;

theorem Th46: :: FILTER_1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being Lattice holds
( ( L1 is C_Lattice & L2 is C_Lattice ) iff [:L1,L2:] is C_Lattice )
proof end;

theorem :: FILTER_1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being Lattice holds
( ( L1 is B_Lattice & L2 is B_Lattice ) iff [:L1,L2:] is B_Lattice )
proof end;

theorem :: FILTER_1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being Lattice holds
( ( L1 is implicative & L2 is implicative ) iff [:L1,L2:] is implicative )
proof end;

theorem :: FILTER_1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being Lattice holds [:L1,L2:] .: = [:(L1 .: ),(L2 .: ):] ;

theorem :: FILTER_1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being Lattice holds [:L1,L2:],[:L2,L1:] are_isomorphic
proof end;

theorem Th51: :: FILTER_1:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B being B_Lattice
for a, b being Element of B holds a <=> b = (a "/\" b) "\/" ((a ` ) "/\" (b ` ))
proof end;

theorem Th52: :: FILTER_1:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B being B_Lattice
for a, b being Element of B holds
( (a => b) ` = a "/\" (b ` ) & (a <=> b) ` = (a "/\" (b ` )) "\/" ((a ` ) "/\" b) & (a <=> b) ` = a <=> (b ` ) & (a <=> b) ` = (a ` ) <=> b )
proof end;

theorem Th53: :: FILTER_1:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B being B_Lattice
for a, b, c being Element of B st a <=> b = a <=> c holds
b = c
proof end;

theorem Th54: :: FILTER_1:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B being B_Lattice
for a, b being Element of B holds a <=> (a <=> b) = b
proof end;

theorem :: FILTER_1:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being I_Lattice
for i, j being Element of I holds
( (i "\/" j) => i = j => i & i => (i "/\" j) = i => j )
proof end;

theorem Th56: :: FILTER_1:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being I_Lattice
for i, j, k being Element of I holds
( i => j [= i => (j "\/" k) & i => j [= (i "/\" k) => j & i => j [= i => (k "\/" j) & i => j [= (k "/\" i) => j )
proof end;

Lm1: for I being I_Lattice
for FI being Filter of I
for i, j, k being Element of I st i => j in FI holds
( i => (j "\/" k) in FI & i => (k "\/" j) in FI & (i "/\" k) => j in FI & (k "/\" i) => j in FI )
proof end;

theorem Th57: :: FILTER_1:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being I_Lattice
for i, k, j being Element of I holds (i => k) "/\" (j => k) [= (i "\/" j) => k
proof end;

Lm2: for I being I_Lattice
for FI being Filter of I
for i, k, j being Element of I st i => k in FI & j => k in FI holds
(i "\/" j) => k in FI
proof end;

theorem Th58: :: FILTER_1:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being I_Lattice
for i, j, k being Element of I holds (i => j) "/\" (i => k) [= i => (j "/\" k)
proof end;

Lm3: for I being I_Lattice
for FI being Filter of I
for i, j, k being Element of I st i => j in FI & i => k in FI holds
i => (j "/\" k) in FI
proof end;

theorem Th59: :: FILTER_1:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being I_Lattice
for FI being Filter of I
for i1, i2, j1, j2 being Element of I st i1 <=> i2 in FI & j1 <=> j2 in FI holds
( (i1 "\/" j1) <=> (i2 "\/" j2) in FI & (i1 "/\" j1) <=> (i2 "/\" j2) in FI )
proof end;

Lm4: for I being I_Lattice
for FI being Filter of I
for i, j being Element of I holds
( i in Class (equivalence_wrt FI),j iff i <=> j in FI )
proof end;

theorem Th60: :: FILTER_1:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being I_Lattice
for FI being Filter of I
for i, k, j being Element of I st i in Class (equivalence_wrt FI),k & j in Class (equivalence_wrt FI),k holds
( i "\/" j in Class (equivalence_wrt FI),k & i "/\" j in Class (equivalence_wrt FI),k )
proof end;

theorem Th61: :: FILTER_1:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B being B_Lattice
for c, d being Element of B holds
( c "\/" (c <=> d) in Class (equivalence_wrt <.d.)),c & ( for b being Element of B st b in Class (equivalence_wrt <.d.)),c holds
b [= c "\/" (c <=> d) ) )
proof end;

theorem :: FILTER_1:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B being B_Lattice
for a being Element of B holds B,[:(B /\/ <.a.)),(latt <.a.)):] are_isomorphic
proof end;