:: FILTER_0 semantic presentation

theorem Th1: :: FILTER_0:1

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

proof end;

theorem Th2: :: FILTER_0:2

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

proof end;

theorem Th3: :: FILTER_0:3

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

proof end;

theorem Th4: :: FILTER_0:4

for b₁ being Lattice
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂ [= b₃ & b₄ [= b₅ holds
( b₂ "\/" b₄ [= b₃ "\/" b₅ & b₂ "\/" b₄ [= b₅ "\/" b₃ )

proof end;

theorem Th5: :: FILTER_0:5

for b₁ being Lattice
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂ [= b₃ & b₄ [= b₅ holds
( b₂ "/\" b₄ [= b₃ "/\" b₅ & b₂ "/\" b₄ [= b₅ "/\" b₃ )

proof end;

theorem Th6: :: FILTER_0:6

for b₁ being Lattice
for b₂, b₃, b₄ being Element of b₁ st b₂ [= b₃ & b₄ [= b₃ holds
b₂ "\/" b₄ [= b₃

proof end;

theorem Th7: :: FILTER_0:7

for b₁ being Lattice
for b₂, b₃, b₄ being Element of b₁ st b₂ [= b₃ & b₂ [= b₄ holds
b₂ [= b₃ "/\" b₄

proof end;

definition

let c₁ be Lattice;
mode Filter of c₁ -> non empty Subset of a₁ means :Def1: :: FILTER_0:def 1
for b₁, b₂ being Element of a₁ holds
( ( b₁ in a₂ & b₂ in a₂ ) iff b₁ "/\" b₂ in a₂ );
existence

proof end;

end;

:: deftheorem Def1 defines Filter FILTER_0:def 1 :

theorem Th8: :: FILTER_0:8

canceled;

theorem Th9: :: FILTER_0:9

for b₁ being Lattice
for b₂ being non empty Subset of b₁ holds
( b₂ is Filter of b₁ iff ( ( for b₃, b₄ being Element of b₁ st b₃ in b₂ & b₄ in b₂ holds
b₃ "/\" b₄ in b₂ ) & ( for b₃, b₄ being Element of b₁ st b₃ in b₂ & b₃ [= b₄ holds
b₄ in b₂ ) ) )

proof end;

theorem Th10: :: FILTER_0:10

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

proof end;

theorem Th11: :: FILTER_0:11

for b₁ being Lattice
for b₂ being Filter of b₁ ex b₃ being Element of b₁ st b₃ in b₂

proof end;

theorem Th12: :: FILTER_0:12

for b₁ being Lattice
for b₂ being Filter of b₁ st b₁ is 1_Lattice holds
Top b₁ in b₂

proof end;

theorem Th13: :: FILTER_0:13

for b₁ being Lattice st b₁ is 1_Lattice holds
{(Top b₁)} is Filter of b₁

proof end;

theorem Th14: :: FILTER_0:14

for b₁ being Lattice
for b₂ being Element of b₁ st {b₂} is Filter of b₁ holds
b₁ is upper-bounded

proof end;

theorem Th15: :: FILTER_0:15

for b₁ being Lattice holds the carrier of b₁ is Filter of b₁

proof end;

definition

let c₁ be Lattice;
func <.c₁.) -> Filter of a₁ equals :: FILTER_0:def 2
the carrier of a₁;
coherence by Th15;

end;

:: deftheorem Def2 defines <. FILTER_0:def 2 :

definition

let c₁ be Lattice;
let c₂ be Element of c₁;
func <.c₂.) -> Filter of a₁ equals :: FILTER_0:def 3
{ b₁ where B is Element of a₁ : a₂ [= b₁ } ;
coherence

proof end;

end;

:: deftheorem Def3 defines <. FILTER_0:def 3 :

theorem Th16: :: FILTER_0:16

canceled;

theorem Th17: :: FILTER_0:17

canceled;

theorem Th18: :: FILTER_0:18

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

proof end;

theorem Th19: :: FILTER_0:19

for b₁ being Lattice
for b₂, b₃ being Element of b₁ holds
( b₂ in <.b₂.) & b₂ "\/" b₃ in <.b₂.) & b₃ "\/" b₂ in <.b₂.) )

proof end;

theorem Th20: :: FILTER_0:20

for b₁ being Lattice st b₁ is 0_Lattice holds
<.b₁.) = <.(Bottom b₁).)

proof end;

definition

let c₁ be Lattice;
let c₂ be Filter of c₁;
attr a₂ is being_ultrafilter means :Def4: :: FILTER_0:def 4
( a₂ <> the carrier of a₁ & ( for b₁ being Filter of a₁ st a₂ c= b₁ & b₁ <> the carrier of a₁ holds
a₂ = b₁ ) );

end;

:: deftheorem Def4 defines being_ultrafilter FILTER_0:def 4 :

notation

let c₁ be Lattice;
let c₂ be Filter of c₁;
synonym c₂ is_ultrafilter for being_ultrafilter c₂;

end;

theorem Th21: :: FILTER_0:21

canceled;

theorem Th22: :: FILTER_0:22

for b₁ being Lattice st b₁ is lower-bounded holds
for b₂ being Filter of b₁ st b₂ <> the carrier of b₁ holds
ex b₃ being Filter of b₁ st
( b₂ c= b₃ & b₃ is_ultrafilter )

proof end;

theorem Th23: :: FILTER_0:23

for b₁ being Lattice
for b₂ being Element of b₁ st ex b₃ being Element of b₁ st b₂ "/\" b₃ <> b₂ holds
<.b₂.) <> the carrier of b₁

proof end;

theorem Th24: :: FILTER_0:24

for b₁ being Lattice
for b₂ being Element of b₁ st b₁ is 0_Lattice & b₂ <> Bottom b₁ holds
ex b₃ being Filter of b₁ st
( b₂ in b₃ & b₃ is_ultrafilter )

proof end;

definition

let c₁ be Lattice;
let c₂ be non empty Subset of c₁;
func <.c₂.) -> Filter of a₁ means :Def5: :: FILTER_0:def 5
( a₂ c= a₃ & ( for b₁ being Filter of a₁ st a₂ c= b₁ holds
a₃ c= b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines <. FILTER_0:def 5 :

theorem Th25: :: FILTER_0:25

canceled;

theorem Th26: :: FILTER_0:26

for b₁ being Lattice
for b₂ being Filter of b₁ holds <.b₂.) = b₂

proof end;

theorem Th27: :: FILTER_0:27

for b₁ being Lattice
for b₂, b₃ being non empty Subset of b₁ st b₂ c= b₃ holds
<.b₂.) c= <.b₃.)

proof end;

theorem Th28: :: FILTER_0:28

canceled;

theorem Th29: :: FILTER_0:29

for b₁ being Lattice
for b₂ being Element of b₁
for b₃ being non empty Subset of b₁ st b₂ in b₃ holds
<.b₂.) c= <.b₃.)

proof end;

theorem Th30: :: FILTER_0:30

for b₁ being Lattice
for b₂ being Element of b₁
for b₃ being non empty Subset of b₁ st b₃ = {b₂} holds
<.b₃.) = <.b₂.)

proof end;

theorem Th31: :: FILTER_0:31

for b₁ being Lattice
for b₂ being non empty Subset of b₁ st b₁ is 0_Lattice & Bottom b₁ in b₂ holds
( <.b₂.) = <.b₁.) & <.b₂.) = the carrier of b₁ )

proof end;

theorem Th32: :: FILTER_0:32

for b₁ being Lattice
for b₂ being Filter of b₁ st b₁ is 0_Lattice & Bottom b₁ in b₂ holds
( b₂ = <.b₁.) & b₂ = the carrier of b₁ )

proof end;

definition

let c₁ be Lattice;
let c₂ be Filter of c₁;
attr a₂ is prime means :: FILTER_0:def 6
for b₁, b₂ being Element of a₁ holds
( b₁ "\/" b₂ in a₂ iff ( b₁ in a₂ or b₂ in a₂ ) );

end;

:: deftheorem Def6 defines prime FILTER_0:def 6 :

theorem Th33: :: FILTER_0:33

canceled;

theorem Th34: :: FILTER_0:34

for b₁ being Lattice st b₁ is B_Lattice holds
for b₂, b₃ being Element of b₁ holds
( b₂ "/\" ((b₂ ` ) "\/" b₃) [= b₃ & ( for b₄ being Element of b₁ st b₂ "/\" b₄ [= b₃ holds
b₄ [= (b₂ ` ) "\/" b₃ ) )

proof end;

definition

let c₁ be non empty LattStr ;
attr a₁ is implicative means :Def7: :: FILTER_0:def 7
for b₁, b₂ being Element of a₁ ex b₃ being Element of a₁ st
( b₁ "/\" b₃ [= b₂ & ( for b₄ being Element of a₁ st b₁ "/\" b₄ [= b₂ holds
b₄ [= b₃ ) );

end;

:: deftheorem Def7 defines implicative FILTER_0:def 7 :

registration

cluster strict implicative LattStr ;
existence

proof end;

end;

definition

mode I_Lattice is implicative Lattice;

end;

definition

let c₁ be Lattice;
let c₂, c₃ be Element of c₁;
assume E27: c₁ is I_Lattice ;
func c₂ => c₃ -> Element of a₁ means :Def8: :: FILTER_0:def 8
( a₂ "/\" a₄ [= a₃ & ( for b₁ being Element of a₁ st a₂ "/\" b₁ [= a₃ holds
b₁ [= a₄ ) );
existence by E27, Def7;
correctness

proof end;

end;

:: deftheorem Def8 defines => FILTER_0:def 8 :

theorem Th35: :: FILTER_0:35

canceled;

theorem Th36: :: FILTER_0:36

canceled;

theorem Th37: :: FILTER_0:37

for b₁ being I_Lattice holds b₁ is upper-bounded

proof end;

theorem Th38: :: FILTER_0:38

for b₁ being I_Lattice
for b₂ being Element of b₁ holds b₂ => b₂ = Top b₁

proof end;

theorem Th39: :: FILTER_0:39

for b₁ being I_Lattice holds b₁ is distributive

proof end;

theorem Th40: :: FILTER_0:40

for b₁ being B_Lattice holds b₁ is implicative

proof end;

registration

cluster implicative -> distributive LattStr ;
coherence by Th39;

end;

theorem Th41: :: FILTER_0:41

for b₁ being I_Lattice
for b₂, b₃ being Element of b₁
for b₄ being Filter of b₁ st b₂ in b₄ & b₂ => b₃ in b₄ holds
b₃ in b₄

proof end;

theorem Th42: :: FILTER_0:42

for b₁ being I_Lattice
for b₂, b₃ being Element of b₁
for b₄ being Filter of b₁ st b₂ in b₄ holds
b₃ => b₂ in b₄

proof end;

definition

let c₁ be Lattice;
let c₂, c₃ be non empty Subset of c₁;
func c₂ "/\" c₃ -> Subset of a₁ equals :: FILTER_0:def 9
{ (b₁ "/\" b₂) where B is Element of a₁, B is Element of a₁ : ( b₁ in a₂ & b₂ in a₃ ) } ;
coherence

proof end;

end;

:: deftheorem Def9 defines "/\" FILTER_0:def 9 :

registration

let c₁ be Lattice;
let c₂, c₃ be non empty Subset of c₁;
cluster a₂ "/\" a₃ -> non empty ;
coherence

proof end;

end;

theorem Th43: :: FILTER_0:43

canceled;

theorem Th44: :: FILTER_0:44

for b₁ being Lattice
for b₂, b₃ being Element of b₁
for b₄, b₅ being non empty Subset of b₁ st b₂ in b₄ & b₃ in b₅ holds
( b₂ "/\" b₃ in b₄ "/\" b₅ & b₃ "/\" b₂ in b₄ "/\" b₅ ) ;

theorem Th45: :: FILTER_0:45

for b₁ being Lattice
for b₂ being set
for b₃, b₄ being non empty Subset of b₁ st b₂ in b₃ "/\" b₄ holds
ex b₅, b₆ being Element of b₁ st
( b₂ = b₅ "/\" b₆ & b₅ in b₃ & b₆ in b₄ ) ;

theorem Th46: :: FILTER_0:46

for b₁ being Lattice
for b₂, b₃ being non empty Subset of b₁ holds b₂ "/\" b₃ = b₃ "/\" b₂

proof end;

definition

let c₁ be D_Lattice;
let c₂, c₃ be Filter of c₁;
redefine func "/\" as c₂ "/\" c₃ -> Filter of a₁;
coherence

proof end;

end;

definition

let c₁ be B_Lattice;
let c₂, c₃ be Filter of c₁;
redefine func "/\" as c₂ "/\" c₃ -> Filter of a₁;
coherence

proof end;

end;

theorem Th47: :: FILTER_0:47

for b₁ being Lattice
for b₂, b₃ being non empty Subset of b₁ holds
( <.(b₂ \/ b₃).) = <.(<.b₂.) \/ b₃).) & <.(b₂ \/ b₃).) = <.(b₂ \/ <.b₃.)).) )

proof end;

theorem Th48: :: FILTER_0:48

for b₁ being Lattice
for b₂, b₃ being Filter of b₁ holds <.(b₂ \/ b₃).) = { b₄ where B is Element of b₁ : ex b₁, b₂ being Element of b₁ st
( b₅ "/\" b₆ [= b₄ & b₅ in b₂ & b₆ in b₃ ) }

proof end;

theorem Th49: :: FILTER_0:49

for b₁ being Lattice
for b₂, b₃ being Filter of b₁ holds
( b₂ c= b₂ "/\" b₃ & b₃ c= b₂ "/\" b₃ )

proof end;

theorem Th50: :: FILTER_0:50

for b₁ being Lattice
for b₂, b₃ being Filter of b₁ holds <.(b₂ \/ b₃).) = <.(b₂ "/\" b₃).)

proof end;

theorem Th51: :: FILTER_0:51

for b₁ being I_Lattice
for b₂, b₃ being Filter of b₁ holds <.(b₂ \/ b₃).) = b₂ "/\" b₃

proof end;

theorem Th52: :: FILTER_0:52

for b₁ being B_Lattice
for b₂, b₃ being Filter of b₁ holds <.(b₂ \/ b₃).) = b₂ "/\" b₃

proof end;

theorem Th53: :: FILTER_0:53

for b₁ being I_Lattice
for b₂, b₃ being Element of b₁
for b₄ being non empty Subset of b₁ st b₂ in <.(b₄ \/ {b₃}).) holds
b₃ => b₂ in <.b₄.)

proof end;

theorem Th54: :: FILTER_0:54

for b₁ being I_Lattice
for b₂, b₃, b₄ being Element of b₁
for b₅ being Filter of b₁ st b₂ => b₃ in b₅ & b₃ => b₄ in b₅ holds
b₂ => b₄ in b₅

proof end;

theorem Th55: :: FILTER_0:55

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

proof end;

theorem Th56: :: FILTER_0:56

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds
( b₂ [= b₃ iff b₂ "/\" (b₃ ` ) = Bottom b₁ )

proof end;

theorem Th57: :: FILTER_0:57

for b₁ being B_Lattice
for b₂ being Filter of b₁ holds
( b₂ is_ultrafilter iff ( b₂ <> the carrier of b₁ & ( for b₃ being Element of b₁ holds
( b₃ in b₂ or b₃ ` in b₂ ) ) ) )

proof end;

theorem Th58: :: FILTER_0:58

for b₁ being B_Lattice
for b₂ being Filter of b₁ holds
( ( b₂ <> <.b₁.) & b₂ is prime ) iff b₂ is_ultrafilter )

proof end;

theorem Th59: :: FILTER_0:59

for b₁ being B_Lattice
for b₂ being Filter of b₁ st b₂ is_ultrafilter holds
for b₃ being Element of b₁ holds
( b₃ in b₂ iff not b₃ ` in b₂ )

proof end;

theorem Th60: :: FILTER_0:60

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ st b₂ <> b₃ holds
ex b₄ being Filter of b₁ st
( b₄ is_ultrafilter & ( ( b₂ in b₄ & not b₃ in b₄ ) or ( not b₂ in b₄ & b₃ in b₄ ) ) )

proof end;

definition

let c₁ be Lattice;
let c₂ be Filter of c₁;
func latt c₂ -> Lattice means :Def10: :: FILTER_0:def 10
ex b₁, b₂ being BinOp of a₂ st
( b₁ = the L_join of a₁ || a₂ & b₂ = the L_meet of a₁ || a₂ & a₃ = LattStr(# a₂,b₁,b₂ #) );
uniqueness ;
existence

proof end;

end;

:: deftheorem Def10 defines latt FILTER_0:def 10 :

registration

let c₁ be Lattice;
let c₂ be Filter of c₁;
cluster latt a₂ -> strict ;
coherence

proof end;

end;

theorem Th61: :: FILTER_0:61

canceled;

theorem Th62: :: FILTER_0:62

for b₁ being strict Lattice holds latt <.b₁.) = b₁

proof end;

theorem Th63: :: FILTER_0:63

for b₁ being Lattice
for b₂ being Filter of b₁ holds
( the carrier of (latt b₂) = b₂ & the L_join of (latt b₂) = the L_join of b₁ || b₂ & the L_meet of (latt b₂) = the L_meet of b₁ || b₂ )

proof end;

theorem Th64: :: FILTER_0:64

for b₁ being Lattice
for b₂, b₃ being Element of b₁
for b₄ being Filter of b₁
for b₅, b₆ being Element of (latt b₄) st b₂ = b₅ & b₃ = b₆ holds
( b₂ "\/" b₃ = b₅ "\/" b₆ & b₂ "/\" b₃ = b₅ "/\" b₆ )

proof end;

theorem Th65: :: FILTER_0:65

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

proof end;

theorem Th66: :: FILTER_0:66

for b₁ being Lattice
for b₂ being Filter of b₁ st b₁ is upper-bounded holds
latt b₂ is upper-bounded

proof end;

theorem Th67: :: FILTER_0:67

for b₁ being Lattice
for b₂ being Filter of b₁ st b₁ is modular holds
latt b₂ is modular

proof end;

theorem Th68: :: FILTER_0:68

for b₁ being Lattice
for b₂ being Filter of b₁ st b₁ is distributive holds
latt b₂ is distributive

proof end;

theorem Th69: :: FILTER_0:69

for b₁ being Lattice
for b₂ being Filter of b₁ st b₁ is I_Lattice holds
latt b₂ is implicative

proof end;

theorem Th70: :: FILTER_0:70

for b₁ being Lattice
for b₂ being Element of b₁ holds latt <.b₂.) is lower-bounded

proof end;

theorem Th71: :: FILTER_0:71

for b₁ being Lattice
for b₂ being Element of b₁ holds Bottom (latt <.b₂.)) = b₂

proof end;

theorem Th72: :: FILTER_0:72

for b₁ being Lattice
for b₂ being Element of b₁ st b₁ is upper-bounded holds
Top (latt <.b₂.)) = Top b₁

proof end;

theorem Th73: :: FILTER_0:73

for b₁ being Lattice
for b₂ being Element of b₁ st b₁ is 1_Lattice holds
latt <.b₂.) is bounded

proof end;

theorem Th74: :: FILTER_0:74

for b₁ being Lattice
for b₂ being Element of b₁ st b₁ is C_Lattice & b₁ is M_Lattice holds
latt <.b₂.) is C_Lattice

proof end;

theorem Th75: :: FILTER_0:75

for b₁ being Lattice
for b₂ being Element of b₁ st b₁ is B_Lattice holds
latt <.b₂.) is B_Lattice

proof end;

definition

let c₁ be Lattice;
let c₂, c₃ be Element of c₁;
func c₂ <=> c₃ -> Element of a₁ equals :: FILTER_0:def 11
(a₂ => a₃) "/\" (a₃ => a₂);
correctness ;

end;

:: deftheorem Def11 defines <=> FILTER_0:def 11 :

theorem Th76: :: FILTER_0:76

canceled;

theorem Th77: :: FILTER_0:77

for b₁ being Lattice
for b₂, b₃ being Element of b₁ holds b₂ <=> b₃ = b₃ <=> b₂ ;

theorem Th78: :: FILTER_0:78

for b₁ being I_Lattice
for b₂, b₃, b₄ being Element of b₁
for b₅ being Filter of b₁ st b₂ <=> b₃ in b₅ & b₃ <=> b₄ in b₅ holds
b₂ <=> b₄ in b₅

proof end;

definition

let c₁ be Lattice;
let c₂ be Filter of c₁;
func equivalence_wrt c₂ -> Relation means :Def12: :: FILTER_0:def 12
( field a₃ c= the carrier of a₁ & ( for b₁, b₂ being Element of a₁ holds
( [b₁,b₂] in a₃ iff b₁ <=> b₂ in a₂ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines equivalence_wrt FILTER_0:def 12 :

theorem Th79: :: FILTER_0:79

canceled;

theorem Th80: :: FILTER_0:80

for b₁ being Lattice
for b₂ being Filter of b₁ holds equivalence_wrt b₂ is Relation of the carrier of b₁

proof end;

theorem Th81: :: FILTER_0:81

for b₁ being Lattice
for b₂ being Filter of b₁ st b₁ is I_Lattice holds
equivalence_wrt b₂ is_reflexive_in the carrier of b₁

proof end;

theorem Th82: :: FILTER_0:82

for b₁ being Lattice
for b₂ being Filter of b₁ holds equivalence_wrt b₂ is_symmetric_in the carrier of b₁

proof end;

theorem Th83: :: FILTER_0:83

for b₁ being Lattice
for b₂ being Filter of b₁ st b₁ is I_Lattice holds
equivalence_wrt b₂ is_transitive_in the carrier of b₁

proof end;

theorem Th84: :: FILTER_0:84

for b₁ being Lattice
for b₂ being Filter of b₁ st b₁ is I_Lattice holds
equivalence_wrt b₂ is Equivalence_Relation of the carrier of b₁

proof end;

theorem Th85: :: FILTER_0:85

for b₁ being Lattice
for b₂ being Filter of b₁ st b₁ is I_Lattice holds
field (equivalence_wrt b₂) = the carrier of b₁

proof end;

definition

let c₁ be I_Lattice;
let c₂ be Filter of c₁;
redefine func equivalence_wrt as equivalence_wrt c₂ -> Equivalence_Relation of the carrier of a₁;
coherence by Th84;

end;

definition

let c₁ be B_Lattice;
let c₂ be Filter of c₁;
redefine func equivalence_wrt as equivalence_wrt c₂ -> Equivalence_Relation of the carrier of a₁;
coherence

proof end;

end;

definition

let c₁ be Lattice;
let c₂ be Filter of c₁;
let c₃, c₄ be Element of c₁;
pred c₃,c₄ are_equivalence_wrt c₂ means :Def13: :: FILTER_0:def 13
a₃ <=> a₄ in a₂;

end;

:: deftheorem Def13 defines are_equivalence_wrt FILTER_0:def 13 :

theorem Th86: :: FILTER_0:86

canceled;

theorem Th87: :: FILTER_0:87

for b₁ being Lattice
for b₂, b₃ being Element of b₁
for b₄ being Filter of b₁ holds
( b₂,b₃ are_equivalence_wrt b₄ iff [b₂,b₃] in equivalence_wrt b₄ )

proof end;

theorem Th88: :: FILTER_0:88

for b₁ being B_Lattice
for b₂ being Filter of b₁
for b₃ being I_Lattice
for b₄ being Element of b₃
for b₅ being Filter of b₃
for b₆ being Element of b₁ holds
( b₄,b₄ are_equivalence_wrt b₅ & b₆,b₆ are_equivalence_wrt b₂ )

proof end;

theorem Th89: :: FILTER_0:89

for b₁ being Lattice
for b₂, b₃ being Element of b₁
for b₄ being Filter of b₁ st b₂,b₃ are_equivalence_wrt b₄ holds
b₃,b₂ are_equivalence_wrt b₄

proof end;

theorem Th90: :: FILTER_0:90

for b₁ being B_Lattice
for b₂ being Filter of b₁
for b₃ being I_Lattice
for b₄, b₅, b₆ being Element of b₃
for b₇ being Filter of b₃
for b₈, b₉, b₁₀ being Element of b₁ holds
( ( b₄,b₅ are_equivalence_wrt b₇ & b₅,b₆ are_equivalence_wrt b₇ implies b₄,b₆ are_equivalence_wrt b₇ ) & ( b₈,b₉ are_equivalence_wrt b₂ & b₉,b₁₀ are_equivalence_wrt b₂ implies b₈,b₁₀ are_equivalence_wrt b₂ ) )

proof end;