:: FILTER_1 semantic presentation

deffunc H₁( LattStr ) -> set = the carrier of a₁;

deffunc H₂( LattStr ) -> M5([:the carrier of a₁,the carrier of a₁:],the carrier of a₁) = the L_join of a₁;

deffunc H₃( LattStr ) -> M5([:the carrier of a₁,the carrier of a₁:],the carrier of a₁) = the L_meet of a₁;

theorem Th1: :: FILTER_1:1

for b₁ being Lattice
for b₂, b₃ being Filter of b₁ holds b₂ /\ b₃ is Filter of b₁

proof end;

theorem Th2: :: FILTER_1:2

for b₁ being Lattice
for b₂, b₃ being Element of b₁ st <.b₂.) = <.b₃.) holds
b₂ = b₃

proof end;

definition

let c₁ be Lattice;
let c₂, c₃ be Filter of c₁;
redefine func /\ as c₂ /\ c₃ -> Filter of a₁;
coherence by Th1;

end;

definition

let c₁ be non empty set ;
let c₂ be Relation;
mode UnOp of c₁,c₂ -> UnOp of a₁ means :Def1: :: FILTER_1:def 1
for b₁, b₂ being Element of a₁ st [b₁,b₂] in a₂ holds
[(a₃ . b₁),(a₃ . b₂)] in a₂;
existence

proof end;

mode BinOp of c₁,c₂ -> BinOp of a₁ means :Def2: :: FILTER_1:def 2
for b₁, b₂, b₃, b₄ being Element of a₁ st [b₁,b₂] in a₂ & [b₃,b₄] in a₂ holds
[(a₃ . b₁,b₃),(a₃ . b₂,b₄)] in a₂;
existence

proof end;

end;

:: deftheorem Def1 defines UnOp FILTER_1:def 1 :

:: deftheorem Def2 defines BinOp FILTER_1:def 2 :

definition

let c₁ be non empty set ;
let c₂ be Equivalence_Relation of c₁;
mode UnOp of a₂ is UnOp of a₁,a₂;
mode BinOp of a₂ is BinOp of a₁,a₂;

end;

registration

let c₁ be non empty set ;
let c₂ be Equivalence_Relation of c₁;
cluster Class a₂ -> non empty ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be Equivalence_Relation of c₁;
let c₃ be Element of c₁;
redefine func Class as Class c₂,c₃ -> Element of Class a₂;
coherence by EQREL_1:def 5;

end;

definition

let c₁ be non empty set ;
let c₂ be Equivalence_Relation of c₁;
let c₃ be UnOp of c₁;
assume E4: c₃ is UnOp of c₁,c₂ ;
func c₃ /\/ c₂ -> UnOp of Class a₂ means :: FILTER_1:def 3
for b₁, b₂ being set st b₁ in Class a₂ & b₂ in b₁ holds
a₄ . b₁ = Class a₂,(a₃ . b₂);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines /\/ FILTER_1:def 3 :

definition

let c₁ be non empty set ;
let c₂ be Equivalence_Relation of c₁;
let c₃ be BinOp of c₁;
assume E4: c₃ is BinOp of c₁,c₂ ;
func c₃ /\/ c₂ -> BinOp of Class a₂ means :Def4: :: FILTER_1:def 4
for b₁, b₂, b₃, b₄ being set st b₁ in Class a₂ & b₂ in Class a₂ & b₃ in b₁ & b₄ in b₂ holds
a₄ . b₁,b₂ = Class a₂,(a₃ . b₃,b₄);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines /\/ FILTER_1:def 4 :

theorem Th3: :: FILTER_1:3

for b₁ being non empty set
for b₂ being Equivalence_Relation of b₁
for b₃, b₄ being Element of b₁
for b₅ being BinOp of b₁,b₂ holds (b₅ /\/ b₂) . (Class b₂,b₃),(Class b₂,b₄) = Class b₂,(b₅ . b₃,b₄)

proof end;

scheme :: FILTER_1:sch 1
s1{ F₁() -> non empty set , F₂() -> Equivalence_Relation of F₁(), P₁[ set ] } :

for b₁ being Element of Class F₂() holds P₁[b₁]

provided

E6: for b₁ being Element of F₁() holds P₁[ Class F₂(),b₁]

proof end;

scheme :: FILTER_1:sch 2
s2{ F₁() -> non empty set , F₂() -> Equivalence_Relation of F₁(), P₁[ set , set ] } :

for b₁, b₂ being Element of Class F₂() holds P₁[b₁,b₂]

provided

E6: for b₁, b₂ being Element of F₁() holds P₁[ Class F₂(),b₁, Class F₂(),b₂]

proof end;

scheme :: FILTER_1:sch 3
s3{ F₁() -> non empty set , F₂() -> Equivalence_Relation of F₁(), P₁[ set , set , set ] } :

for b₁, b₂, b₃ being Element of Class F₂() holds P₁[b₁,b₂,b₃]

provided

E6: for b₁, b₂, b₃ being Element of F₁() holds P₁[ Class F₂(),b₁, Class F₂(),b₂, Class F₂(),b₃]

proof end;

theorem Th4: :: FILTER_1:4

for b₁ being non empty set
for b₂ being Equivalence_Relation of b₁
for b₃ being BinOp of b₁,b₂ st b₃ is commutative holds
b₃ /\/ b₂ is commutative

proof end;

theorem Th5: :: FILTER_1:5

for b₁ being non empty set
for b₂ being Equivalence_Relation of b₁
for b₃ being BinOp of b₁,b₂ st b₃ is associative holds
b₃ /\/ b₂ is associative

proof end;

theorem Th6: :: FILTER_1:6

for b₁ being non empty set
for b₂ being Equivalence_Relation of b₁
for b₃ being Element of b₁
for b₄ being BinOp of b₁,b₂ st b₃ is_a_left_unity_wrt b₄ holds
Class b₂,b₃ is_a_left_unity_wrt b₄ /\/ b₂

proof end;

theorem Th7: :: FILTER_1:7

for b₁ being non empty set
for b₂ being Equivalence_Relation of b₁
for b₃ being Element of b₁
for b₄ being BinOp of b₁,b₂ st b₃ is_a_right_unity_wrt b₄ holds
Class b₂,b₃ is_a_right_unity_wrt b₄ /\/ b₂

proof end;

theorem Th8: :: FILTER_1:8

for b₁ being non empty set
for b₂ being Equivalence_Relation of b₁
for b₃ being Element of b₁
for b₄ being BinOp of b₁,b₂ st b₃ is_a_unity_wrt b₄ holds
Class b₂,b₃ is_a_unity_wrt b₄ /\/ b₂

proof end;

theorem Th9: :: FILTER_1:9

for b₁ being non empty set
for b₂ being Equivalence_Relation of b₁
for b₃, b₄ being BinOp of b₁,b₂ st b₃ is_left_distributive_wrt b₄ holds
b₃ /\/ b₂ is_left_distributive_wrt b₄ /\/ b₂

proof end;

theorem Th10: :: FILTER_1:10

for b₁ being non empty set
for b₂ being Equivalence_Relation of b₁
for b₃, b₄ being BinOp of b₁,b₂ st b₃ is_right_distributive_wrt b₄ holds
b₃ /\/ b₂ is_right_distributive_wrt b₄ /\/ b₂

proof end;

theorem Th11: :: FILTER_1:11

for b₁ being non empty set
for b₂ being Equivalence_Relation of b₁
for b₃, b₄ being BinOp of b₁,b₂ st b₃ is_distributive_wrt b₄ holds
b₃ /\/ b₂ is_distributive_wrt b₄ /\/ b₂

proof end;

theorem Th12: :: FILTER_1:12

for b₁ being non empty set
for b₂ being Equivalence_Relation of b₁
for b₃, b₄ being BinOp of b₁,b₂ st b₃ absorbs b₄ holds
b₃ /\/ b₂ absorbs b₄ /\/ b₂

proof end;

theorem Th13: :: FILTER_1:13

for b₁ being I_Lattice
for b₂ being Filter of b₁ holds the L_join of b₁ is BinOp of the carrier of b₁, equivalence_wrt b₂

proof end;

theorem Th14: :: FILTER_1:14

for b₁ being I_Lattice
for b₂ being Filter of b₁ holds the L_meet of b₁ is BinOp of the carrier of b₁, equivalence_wrt b₂

proof end;

definition

let c₁ be Lattice;
let c₂ be Filter of c₁;
assume E15: c₁ is I_Lattice ;
func c₁ /\/ c₂ -> strict Lattice means :Def5: :: FILTER_1:def 5
for b₁ being Equivalence_Relation of the carrier of a₁ st b₁ = equivalence_wrt a₂ holds
a₃ = LattStr(# (Class b₁),(the L_join of a₁ /\/ b₁),(the L_meet of a₁ /\/ b₁) #);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines /\/ FILTER_1:def 5 :

definition

let c₁ be Lattice;
let c₂ be Filter of c₁;
let c₃ be Element of c₁;
assume E16: c₁ is I_Lattice ;
func c₃ /\/ c₂ -> Element of (a₁ /\/ a₂) means :Def6: :: FILTER_1:def 6
for b₁ being Equivalence_Relation of the carrier of a₁ st b₁ = equivalence_wrt a₂ holds
a₄ = Class b₁,a₃;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines /\/ FILTER_1:def 6 :

theorem Th15: :: FILTER_1:15

for b₁ being I_Lattice
for b₂ being Filter of b₁
for b₃, b₄ being Element of b₁ holds
( (b₃ /\/ b₂) "\/" (b₄ /\/ b₂) = (b₃ "\/" b₄) /\/ b₂ & (b₃ /\/ b₂) "/\" (b₄ /\/ b₂) = (b₃ "/\" b₄) /\/ b₂ )

proof end;

theorem Th16: :: FILTER_1:16

for b₁ being I_Lattice
for b₂ being Filter of b₁
for b₃, b₄ being Element of b₁ holds
( b₃ /\/ b₂ [= b₄ /\/ b₂ iff b₃ => b₄ in b₂ )

proof end;

theorem Th17: :: FILTER_1:17

for b₁ being I_Lattice
for b₂, b₃, b₄ being Element of b₁ holds (b₂ "/\" b₃) => b₄ = b₂ => (b₃ => b₄)

proof end;

theorem Th18: :: FILTER_1:18

for b₁ being I_Lattice
for b₂ being Filter of b₁ st b₁ is lower-bounded holds
( b₁ /\/ b₂ is 0_Lattice & Bottom (b₁ /\/ b₂) = (Bottom b₁) /\/ b₂ )

proof end;

theorem Th19: :: FILTER_1:19

for b₁ being I_Lattice
for b₂ being Filter of b₁ holds
( b₁ /\/ b₂ is 1_Lattice & Top (b₁ /\/ b₂) = (Top b₁) /\/ b₂ )

proof end;

theorem Th20: :: FILTER_1:20

for b₁ being I_Lattice
for b₂ being Filter of b₁ holds b₁ /\/ b₂ is implicative

proof end;

theorem Th21: :: FILTER_1:21

for b₁ being B_Lattice
for b₂ being Filter of b₁ holds b₁ /\/ b₂ is B_Lattice

proof end;

definition

let c₁, c₂ be set ;
let c₃ be BinOp of c₁;
let c₄ be BinOp of c₂;
redefine func |: as |:c₃,c₄:| -> BinOp of [:a₁,a₂:];
coherence

proof end;

end;

theorem Th22: :: FILTER_1:22

for b₁, b₂ being non empty set
for b₃, b₄ being Element of b₁
for b₅, b₆ being Element of b₂
for b₇ being BinOp of b₁
for b₈ being BinOp of b₂ holds |:b₇,b₈:| . [b₃,b₅],[b₄,b₆] = [(b₇ . b₃,b₄),(b₈ . b₅,b₆)]

proof end;

scheme :: FILTER_1:sch 4
s4{ F₁() -> non empty set , F₂() -> non empty set , P₁[ set ] } :

for b₁ being Element of [:F₁(),F₂():] holds P₁[b₁]

provided

E24: for b₁ being Element of F₁()
for b₂ being Element of F₂() holds P₁[[b₁,b₂]]

proof end;

scheme :: FILTER_1:sch 5
s5{ F₁() -> non empty set , F₂() -> non empty set , P₁[ set , set ] } :

for b₁, b₂ being Element of [:F₁(),F₂():] holds P₁[b₁,b₂]

provided

E24: for b₁, b₂ being Element of F₁()
for b₃, b₄ being Element of F₂() holds P₁[[b₁,b₃],[b₂,b₄]]

proof end;

scheme :: FILTER_1:sch 6
s6{ F₁() -> non empty set , F₂() -> non empty set , P₁[ set , set , set ] } :

for b₁, b₂, b₃ being Element of [:F₁(),F₂():] holds P₁[b₁,b₂,b₃]

provided

E24: for b₁, b₂, b₃ being Element of F₁()
for b₄, b₅, b₆ being Element of F₂() holds P₁[[b₁,b₄],[b₂,b₅],[b₃,b₆]]

proof end;

theorem Th23: :: FILTER_1:23

for b₁, b₂ being non empty set
for b₃ being BinOp of b₁
for b₄ being BinOp of b₂ holds
( ( b₃ is commutative & b₄ is commutative ) iff |:b₃,b₄:| is commutative )

proof end;

theorem Th24: :: FILTER_1:24

for b₁, b₂ being non empty set
for b₃ being BinOp of b₁
for b₄ being BinOp of b₂ holds
( ( b₃ is associative & b₄ is associative ) iff |:b₃,b₄:| is associative )

proof end;

theorem Th25: :: FILTER_1:25

for b₁, b₂ being non empty set
for b₃ being Element of b₁
for b₄ being Element of b₂
for b₅ being BinOp of b₁
for b₆ being BinOp of b₂ holds
( ( b₃ is_a_left_unity_wrt b₅ & b₄ is_a_left_unity_wrt b₆ ) iff [b₃,b₄] is_a_left_unity_wrt |:b₅,b₆:| )

proof end;

theorem Th26: :: FILTER_1:26

for b₁, b₂ being non empty set
for b₃ being Element of b₁
for b₄ being Element of b₂
for b₅ being BinOp of b₁
for b₆ being BinOp of b₂ holds
( ( b₃ is_a_right_unity_wrt b₅ & b₄ is_a_right_unity_wrt b₆ ) iff [b₃,b₄] is_a_right_unity_wrt |:b₅,b₆:| )

proof end;

theorem Th27: :: FILTER_1:27

for b₁, b₂ being non empty set
for b₃ being Element of b₁
for b₄ being Element of b₂
for b₅ being BinOp of b₁
for b₆ being BinOp of b₂ holds
( ( b₃ is_a_unity_wrt b₅ & b₄ is_a_unity_wrt b₆ ) iff [b₃,b₄] is_a_unity_wrt |:b₅,b₆:| )

proof end;

theorem Th28: :: FILTER_1:28

for b₁, b₂ being non empty set
for b₃, b₄ being BinOp of b₁
for b₅, b₆ being BinOp of b₂ holds
( ( b₃ is_left_distributive_wrt b₄ & b₅ is_left_distributive_wrt b₆ ) iff |:b₃,b₅:| is_left_distributive_wrt |:b₄,b₆:| )

proof end;

theorem Th29: :: FILTER_1:29

for b₁, b₂ being non empty set
for b₃, b₄ being BinOp of b₁
for b₅, b₆ being BinOp of b₂ holds
( ( b₃ is_right_distributive_wrt b₄ & b₅ is_right_distributive_wrt b₆ ) iff |:b₃,b₅:| is_right_distributive_wrt |:b₄,b₆:| )

proof end;

theorem Th30: :: FILTER_1:30

for b₁, b₂ being non empty set
for b₃, b₄ being BinOp of b₁
for b₅, b₆ being BinOp of b₂ holds
( ( b₃ is_distributive_wrt b₄ & b₅ is_distributive_wrt b₆ ) iff |:b₃,b₅:| is_distributive_wrt |:b₄,b₆:| )

proof end;

theorem Th31: :: FILTER_1:31

for b₁, b₂ being non empty set
for b₃, b₄ being BinOp of b₁
for b₅, b₆ being BinOp of b₂ holds
( ( b₃ absorbs b₄ & b₅ absorbs b₆ ) iff |:b₃,b₅:| absorbs |:b₄,b₆:| )

proof end;

definition

let c₁, c₂ be non empty LattStr ;
func [:c₁,c₂:] -> strict LattStr equals :: FILTER_1:def 7
LattStr(# [:the carrier of a₁,the carrier of a₂:],|:the L_join of a₁,the L_join of a₂:|,|:the L_meet of a₁,the L_meet of a₂:| #);
correctness ;

end;

:: deftheorem Def7 defines [: FILTER_1:def 7 :

registration

let c₁, c₂ be non empty LattStr ;
cluster [:a₁,a₂:] -> non empty strict ;
coherence ;

end;

definition

let c₁ be Lattice;
func LattRel c₁ -> Relation equals :: FILTER_1:def 8
{ [b₁,b₂] where B is Element of a₁, B is Element of a₁ : b₁ [= b₂ } ;
coherence

proof end;

end;

:: deftheorem Def8 defines LattRel FILTER_1:def 8 :

theorem Th32: :: FILTER_1:32

for b₁ being Lattice
for b₂, b₃ being Element of b₁ holds
( [b₂,b₃] in LattRel b₁ iff b₂ [= b₃ )

proof end;

theorem Th33: :: FILTER_1:33

for b₁ being Lattice holds
( dom (LattRel b₁) = the carrier of b₁ & rng (LattRel b₁) = the carrier of b₁ & field (LattRel b₁) = the carrier of b₁ )

proof end;

definition

let c₁, c₂ be Lattice;
pred c₁,c₂ are_isomorphic means :: FILTER_1:def 9
LattRel a₁, LattRel a₂ are_isomorphic ;
reflexivity by WELLORD1:48;
symmetry by WELLORD1:50;

end;

:: deftheorem Def9 defines are_isomorphic FILTER_1:def 9 :

registration

let c₁, c₂ be Lattice;
cluster [:a₁,a₂:] -> non empty strict Lattice-like ;
coherence

proof end;

end;

theorem Th34: :: FILTER_1:34

for b₁, b₂, b₃ being Lattice st b₁,b₂ are_isomorphic & b₂,b₃ are_isomorphic holds
b₁,b₃ are_isomorphic

proof end;

theorem Th35: :: FILTER_1:35

for b₁, b₂ being non empty LattStr st [:b₁,b₂:] is Lattice holds
( b₁ is Lattice & b₂ is Lattice )

proof end;

definition

let c₁, c₂ be Lattice;
let c₃ be Element of c₁;
let c₄ be Element of c₂;
redefine func [ as [c₃,c₄] -> Element of [:a₁,a₂:];
coherence

proof end;

end;

theorem Th36: :: FILTER_1:36

for b₁, b₂ being Lattice
for b₃, b₄ being Element of b₁
for b₅, b₆ being Element of b₂ holds
( [b₃,b₅] "\/" [b₄,b₆] = [(b₃ "\/" b₄),(b₅ "\/" b₆)] & [b₃,b₅] "/\" [b₄,b₆] = [(b₃ "/\" b₄),(b₅ "/\" b₆)] ) by Th22;

theorem Th37: :: FILTER_1:37

for b₁, b₂ being Lattice
for b₃, b₄ being Element of b₁
for b₅, b₆ being Element of b₂ holds
( [b₃,b₅] [= [b₄,b₆] iff ( b₃ [= b₄ & b₅ [= b₆ ) )

proof end;

theorem Th38: :: FILTER_1:38

for b₁, b₂ being Lattice holds
( ( b₁ is modular & b₂ is modular ) iff [:b₁,b₂:] is modular )

proof end;

theorem Th39: :: FILTER_1:39

for b₁, b₂ being Lattice holds
( ( b₁ is D_Lattice & b₂ is D_Lattice ) iff [:b₁,b₂:] is D_Lattice )

proof end;

theorem Th40: :: FILTER_1:40

for b₁, b₂ being Lattice holds
( ( b₁ is lower-bounded & b₂ is lower-bounded ) iff [:b₁,b₂:] is lower-bounded )

proof end;

theorem Th41: :: FILTER_1:41

for b₁, b₂ being Lattice holds
( ( b₁ is upper-bounded & b₂ is upper-bounded ) iff [:b₁,b₂:] is upper-bounded )

proof end;

theorem Th42: :: FILTER_1:42

for b₁, b₂ being Lattice holds
( ( b₁ is bounded & b₂ is bounded ) iff [:b₁,b₂:] is bounded )

proof end;

theorem Th43: :: FILTER_1:43

for b₁, b₂ being Lattice st b₁ is 0_Lattice & b₂ is 0_Lattice holds
Bottom [:b₁,b₂:] = [(Bottom b₁),(Bottom b₂)]

proof end;

theorem Th44: :: FILTER_1:44

for b₁, b₂ being Lattice st b₁ is 1_Lattice & b₂ is 1_Lattice holds
Top [:b₁,b₂:] = [(Top b₁),(Top b₂)]

proof end;

theorem Th45: :: FILTER_1:45

for b₁, b₂ being Lattice
for b₃, b₄ being Element of b₁
for b₅, b₆ being Element of b₂ st b₁ is 01_Lattice & b₂ is 01_Lattice holds
( ( b₃ is_a_complement_of b₄ & b₅ is_a_complement_of b₆ ) iff [b₃,b₅] is_a_complement_of [b₄,b₆] )

proof end;

theorem Th46: :: FILTER_1:46

for b₁, b₂ being Lattice holds
( ( b₁ is C_Lattice & b₂ is C_Lattice ) iff [:b₁,b₂:] is C_Lattice )

proof end;

theorem Th47: :: FILTER_1:47

for b₁, b₂ being Lattice holds
( ( b₁ is B_Lattice & b₂ is B_Lattice ) iff [:b₁,b₂:] is B_Lattice )

proof end;

theorem Th48: :: FILTER_1:48

for b₁, b₂ being Lattice holds
( ( b₁ is implicative & b₂ is implicative ) iff [:b₁,b₂:] is implicative )

proof end;

theorem Th49: :: FILTER_1:49

for b₁, b₂ being Lattice holds [:b₁,b₂:] .: = [:(b₁ .: ),(b₂ .: ):] ;

theorem Th50: :: FILTER_1:50

for b₁, b₂ being Lattice holds [:b₁,b₂:],[:b₂,b₁:] are_isomorphic

proof end;

theorem Th51: :: FILTER_1:51

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds b₂ <=> b₃ = (b₂ "/\" b₃) "\/" ((b₂ ` ) "/\" (b₃ ` ))

proof end;

theorem Th52: :: FILTER_1:52

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds
( (b₂ => b₃) ` = b₂ "/\" (b₃ ` ) & (b₂ <=> b₃) ` = (b₂ "/\" (b₃ ` )) "\/" ((b₂ ` ) "/\" b₃) & (b₂ <=> b₃) ` = b₂ <=> (b₃ ` ) & (b₂ <=> b₃) ` = (b₂ ` ) <=> b₃ )

proof end;

theorem Th53: :: FILTER_1:53

for b₁ being B_Lattice
for b₂, b₃, b₄ being Element of b₁ st b₂ <=> b₃ = b₂ <=> b₄ holds
b₃ = b₄

proof end;

theorem Th54: :: FILTER_1:54

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds b₂ <=> (b₂ <=> b₃) = b₃

proof end;

theorem Th55: :: FILTER_1:55

for b₁ being I_Lattice
for b₂, b₃ being Element of b₁ holds
( (b₂ "\/" b₃) => b₂ = b₃ => b₂ & b₂ => (b₂ "/\" b₃) = b₂ => b₃ )

proof end;

theorem Th56: :: FILTER_1:56

for b₁ being I_Lattice
for b₂, b₃, b₄ being Element of b₁ holds
( b₂ => b₃ [= b₂ => (b₃ "\/" b₄) & b₂ => b₃ [= (b₂ "/\" b₄) => b₃ & b₂ => b₃ [= b₂ => (b₄ "\/" b₃) & b₂ => b₃ [= (b₄ "/\" b₂) => b₃ )

proof end;

Lemma49: for b₁ being I_Lattice
for b₂ being Filter of b₁
for b₃, b₄, b₅ being Element of b₁ st b₃ => b₄ in b₂ holds
( b₃ => (b₄ "\/" b₅) in b₂ & b₃ => (b₅ "\/" b₄) in b₂ & (b₃ "/\" b₅) => b₄ in b₂ & (b₅ "/\" b₃) => b₄ in b₂ )

proof end;

theorem Th57: :: FILTER_1:57

for b₁ being I_Lattice
for b₂, b₃, b₄ being Element of b₁ holds (b₂ => b₃) "/\" (b₄ => b₃) [= (b₂ "\/" b₄) => b₃

proof end;

Lemma51: for b₁ being I_Lattice
for b₂ being Filter of b₁
for b₃, b₄, b₅ being Element of b₁ st b₃ => b₄ in b₂ & b₅ => b₄ in b₂ holds
(b₃ "\/" b₅) => b₄ in b₂

proof end;

theorem Th58: :: FILTER_1:58

for b₁ being I_Lattice
for b₂, b₃, b₄ being Element of b₁ holds (b₂ => b₃) "/\" (b₂ => b₄) [= b₂ => (b₃ "/\" b₄)

proof end;

Lemma53: for b₁ being I_Lattice
for b₂ being Filter of b₁
for b₃, b₄, b₅ being Element of b₁ st b₃ => b₄ in b₂ & b₃ => b₅ in b₂ holds
b₃ => (b₄ "/\" b₅) in b₂

proof end;

theorem Th59: :: FILTER_1:59

for b₁ being I_Lattice
for b₂ being Filter of b₁
for b₃, b₄, b₅, b₆ being Element of b₁ st b₃ <=> b₄ in b₂ & b₅ <=> b₆ in b₂ holds
( (b₃ "\/" b₅) <=> (b₄ "\/" b₆) in b₂ & (b₃ "/\" b₅) <=> (b₄ "/\" b₆) in b₂ )

proof end;

Lemma55: for b₁ being I_Lattice
for b₂ being Filter of b₁
for b₃, b₄ being Element of b₁ holds
( b₃ in Class (equivalence_wrt b₂),b₄ iff b₃ <=> b₄ in b₂ )

proof end;

theorem Th60: :: FILTER_1:60

for b₁ being I_Lattice
for b₂ being Filter of b₁
for b₃, b₄, b₅ being Element of b₁ st b₃ in Class (equivalence_wrt b₂),b₄ & b₅ in Class (equivalence_wrt b₂),b₄ holds
( b₃ "\/" b₅ in Class (equivalence_wrt b₂),b₄ & b₃ "/\" b₅ in Class (equivalence_wrt b₂),b₄ )

proof end;

theorem Th61: :: FILTER_1:61

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds
( b₂ "\/" (b₂ <=> b₃) in Class (equivalence_wrt <.b₃.)),b₂ & ( for b₄ being Element of b₁ st b₄ in Class (equivalence_wrt <.b₃.)),b₂ holds
b₄ [= b₂ "\/" (b₂ <=> b₃) ) )

proof end;

theorem Th62: :: FILTER_1:62

for b₁ being B_Lattice
for b₂ being Element of b₁ holds b₁,[:(b₁ /\/ <.b₂.)),(latt <.b₂.)):] are_isomorphic

proof end;