:: J\'onsson Theorem about Representation of Modular Lattices
:: by Mariusz {\L}api\'nski
::
:: Copyright (c) 2000-2021 Association of Mizar Users

definition
let L be RelStr ;
attr L is finitely_typed means :Def1: :: LATTICE8:def 1
ex A being non empty set st
( ( for e being object st e in the carrier of L holds
e is Equivalence_Relation of A ) & ex o being Element of NAT st
for e1, e2 being Equivalence_Relation of A
for x, y being object st e1 in the carrier of L & e2 in the carrier of L & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of A st
( len F = o & x,y are_joint_by F,e1,e2 ) );
end;

:: deftheorem Def1 defines finitely_typed LATTICE8:def 1 :
for L being RelStr holds
( L is finitely_typed iff ex A being non empty set st
( ( for e being object st e in the carrier of L holds
e is Equivalence_Relation of A ) & ex o being Element of NAT st
for e1, e2 being Equivalence_Relation of A
for x, y being object st e1 in the carrier of L & e2 in the carrier of L & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of A st
( len F = o & x,y are_joint_by F,e1,e2 ) ) );

definition
let L be lower-bounded LATTICE;
let n be Element of NAT ;
pred L has_a_representation_of_type<= n means :: LATTICE8:def 2
ex A being non trivial set ex f being Homomorphism of L,() st
( f is V17() & Image f is finitely_typed & ex e being Equivalence_Relation of A st
( e in the carrier of () & e <> id A ) & type_of () <= n );
end;

:: deftheorem defines has_a_representation_of_type<= LATTICE8:def 2 :
for L being lower-bounded LATTICE
for n being Element of NAT holds
( L has_a_representation_of_type<= n iff ex A being non trivial set ex f being Homomorphism of L,() st
( f is V17() & Image f is finitely_typed & ex e being Equivalence_Relation of A st
( e in the carrier of () & e <> id A ) & type_of () <= n ) );

registration
existence
ex b1 being LATTICE st
( b1 is lower-bounded & b1 is distributive & b1 is finite )
proof end;
end;

Lm1: 1 is odd
proof end;

Lm2: 2 is even
proof end;

registration
let A be non trivial set ;
existence
ex b1 being non empty Sublattice of EqRelLATT A st
( not b1 is trivial & b1 is finitely_typed & b1 is full )
proof end;
end;

theorem Th1: :: LATTICE8:1
for A being non empty set
for L being lower-bounded LATTICE
for d being distance_function of A,L holds succ {} c= DistEsti d
proof end;

theorem :: LATTICE8:2
for L being trivial Semilattice holds L is modular by STRUCT_0:def 10;

theorem :: LATTICE8:3
for A being non empty set
for L being non empty Sublattice of EqRelLATT A holds
( L is trivial or ex e being Equivalence_Relation of A st
( e in the carrier of L & e <> id A ) )
proof end;

theorem :: LATTICE8:4
for L1, L2 being lower-bounded LATTICE
for f being Function of L1,L2 st f is infs-preserving & f is sups-preserving holds
( f is meet-preserving & f is join-preserving ) ;

theorem Th5: :: LATTICE8:5
for L1, L2 being lower-bounded LATTICE st L1,L2 are_isomorphic & L1 is modular holds
L2 is modular
proof end;

theorem Th6: :: LATTICE8:6
for S being non empty lower-bounded Poset
for T being non empty Poset
for f being monotone Function of S,T holds Image f is lower-bounded
proof end;

theorem Th7: :: LATTICE8:7
for L being lower-bounded LATTICE
for x, y being Element of L
for A being non empty set
for f being Homomorphism of L,() st f is V17() & () . x <= () . y holds
x <= y
proof end;

theorem Th8: :: LATTICE8:8
for A being non trivial set
for L being non empty full finitely_typed Sublattice of EqRelLATT A
for e being Equivalence_Relation of A st e in the carrier of L & e <> id A & type_of L <= 2 holds
L is modular
proof end;

theorem Th9: :: LATTICE8:9
for L being lower-bounded LATTICE st L has_a_representation_of_type<= 2 holds
L is modular
proof end;

:: <= :: L is modular implies L has_a_representation_of_type<= 2
definition
let A be set ;
func new_set2 A -> set equals :: LATTICE8:def 3
A \/ {{A},{{A}}};
correctness
coherence
A \/ {{A},{{A}}} is set
;
;
end;

:: deftheorem defines new_set2 LATTICE8:def 3 :
for A being set holds new_set2 A = A \/ {{A},{{A}}};

registration
let A be set ;
cluster new_set2 A -> non empty ;
coherence
not new_set2 A is empty
;
end;

definition
let A be non empty set ;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be Element of [:A,A, the carrier of L, the carrier of L:];
func new_bi_fun2 (d,q) -> BiFunction of (),L means :Def4: :: LATTICE8:def 4
( ( for u, v being Element of A holds it . (u,v) = d . (u,v) ) & it . ({A},{A}) = Bottom L & it . ({{A}},{{A}}) = Bottom L & it . ({A},{{A}}) = ((d . ((q 1_4),(q 2_4))) "\/" (q 3_4)) "/\" (q 4_4) & it . ({{A}},{A}) = ((d . ((q 1_4),(q 2_4))) "\/" (q 3_4)) "/\" (q 4_4) & ( for u being Element of A holds
( it . (u,{A}) = (d . (u,(q 1_4))) "\/" (q 3_4) & it . ({A},u) = (d . (u,(q 1_4))) "\/" (q 3_4) & it . (u,{{A}}) = (d . (u,(q 2_4))) "\/" (q 3_4) & it . ({{A}},u) = (d . (u,(q 2_4))) "\/" (q 3_4) ) ) );
existence
ex b1 being BiFunction of (),L st
( ( for u, v being Element of A holds b1 . (u,v) = d . (u,v) ) & b1 . ({A},{A}) = Bottom L & b1 . ({{A}},{{A}}) = Bottom L & b1 . ({A},{{A}}) = ((d . ((q 1_4),(q 2_4))) "\/" (q 3_4)) "/\" (q 4_4) & b1 . ({{A}},{A}) = ((d . ((q 1_4),(q 2_4))) "\/" (q 3_4)) "/\" (q 4_4) & ( for u being Element of A holds
( b1 . (u,{A}) = (d . (u,(q 1_4))) "\/" (q 3_4) & b1 . ({A},u) = (d . (u,(q 1_4))) "\/" (q 3_4) & b1 . (u,{{A}}) = (d . (u,(q 2_4))) "\/" (q 3_4) & b1 . ({{A}},u) = (d . (u,(q 2_4))) "\/" (q 3_4) ) ) )
proof end;
uniqueness
for b1, b2 being BiFunction of (),L st ( for u, v being Element of A holds b1 . (u,v) = d . (u,v) ) & b1 . ({A},{A}) = Bottom L & b1 . ({{A}},{{A}}) = Bottom L & b1 . ({A},{{A}}) = ((d . ((q 1_4),(q 2_4))) "\/" (q 3_4)) "/\" (q 4_4) & b1 . ({{A}},{A}) = ((d . ((q 1_4),(q 2_4))) "\/" (q 3_4)) "/\" (q 4_4) & ( for u being Element of A holds
( b1 . (u,{A}) = (d . (u,(q 1_4))) "\/" (q 3_4) & b1 . ({A},u) = (d . (u,(q 1_4))) "\/" (q 3_4) & b1 . (u,{{A}}) = (d . (u,(q 2_4))) "\/" (q 3_4) & b1 . ({{A}},u) = (d . (u,(q 2_4))) "\/" (q 3_4) ) ) & ( for u, v being Element of A holds b2 . (u,v) = d . (u,v) ) & b2 . ({A},{A}) = Bottom L & b2 . ({{A}},{{A}}) = Bottom L & b2 . ({A},{{A}}) = ((d . ((q 1_4),(q 2_4))) "\/" (q 3_4)) "/\" (q 4_4) & b2 . ({{A}},{A}) = ((d . ((q 1_4),(q 2_4))) "\/" (q 3_4)) "/\" (q 4_4) & ( for u being Element of A holds
( b2 . (u,{A}) = (d . (u,(q 1_4))) "\/" (q 3_4) & b2 . ({A},u) = (d . (u,(q 1_4))) "\/" (q 3_4) & b2 . (u,{{A}}) = (d . (u,(q 2_4))) "\/" (q 3_4) & b2 . ({{A}},u) = (d . (u,(q 2_4))) "\/" (q 3_4) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines new_bi_fun2 LATTICE8:def 4 :
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being Element of [:A,A, the carrier of L, the carrier of L:]
for b5 being BiFunction of (),L holds
( b5 = new_bi_fun2 (d,q) iff ( ( for u, v being Element of A holds b5 . (u,v) = d . (u,v) ) & b5 . ({A},{A}) = Bottom L & b5 . ({{A}},{{A}}) = Bottom L & b5 . ({A},{{A}}) = ((d . ((q 1_4),(q 2_4))) "\/" (q 3_4)) "/\" (q 4_4) & b5 . ({{A}},{A}) = ((d . ((q 1_4),(q 2_4))) "\/" (q 3_4)) "/\" (q 4_4) & ( for u being Element of A holds
( b5 . (u,{A}) = (d . (u,(q 1_4))) "\/" (q 3_4) & b5 . ({A},u) = (d . (u,(q 1_4))) "\/" (q 3_4) & b5 . (u,{{A}}) = (d . (u,(q 2_4))) "\/" (q 3_4) & b5 . ({{A}},u) = (d . (u,(q 2_4))) "\/" (q 3_4) ) ) ) );

theorem Th10: :: LATTICE8:10
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L st d is zeroed holds
for q being Element of [:A,A, the carrier of L, the carrier of L:] holds new_bi_fun2 (d,q) is zeroed
proof end;

theorem Th11: :: LATTICE8:11
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L st d is symmetric holds
for q being Element of [:A,A, the carrier of L, the carrier of L:] holds new_bi_fun2 (d,q) is symmetric
proof end;

theorem Th12: :: LATTICE8:12
for A being non empty set
for L being lower-bounded LATTICE st L is modular holds
for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds
for q being Element of [:A,A, the carrier of L, the carrier of L:] st d . ((q 1_4),(q 2_4)) <= (q 3_4) "\/" (q 4_4) holds
new_bi_fun2 (d,q) is u.t.i.
proof end;

theorem Th13: :: LATTICE8:13
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being Element of [:A,A, the carrier of L, the carrier of L:] holds d c= new_bi_fun2 (d,q)
proof end;

definition
let A be non empty set ;
let O be Ordinal;
func ConsecutiveSet2 (A,O) -> set means :Def5: :: LATTICE8:def 5
ex L0 being Sequence st
( it = last L0 & dom L0 = succ O & L0 . 0 = A & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_set2 (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> 0 & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) );
correctness
existence
ex b1 being set ex L0 being Sequence st
( b1 = last L0 & dom L0 = succ O & L0 . 0 = A & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_set2 (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> 0 & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) )
;
uniqueness
for b1, b2 being set st ex L0 being Sequence st
( b1 = last L0 & dom L0 = succ O & L0 . 0 = A & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_set2 (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> 0 & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) ) & ex L0 being Sequence st
( b2 = last L0 & dom L0 = succ O & L0 . 0 = A & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_set2 (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> 0 & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def5 defines ConsecutiveSet2 LATTICE8:def 5 :
for A being non empty set
for O being Ordinal
for b3 being set holds
( b3 = ConsecutiveSet2 (A,O) iff ex L0 being Sequence st
( b3 = last L0 & dom L0 = succ O & L0 . 0 = A & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_set2 (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> 0 & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) ) );

theorem Th14: :: LATTICE8:14
for A being non empty set holds ConsecutiveSet2 (A,0) = A
proof end;

theorem Th15: :: LATTICE8:15
for A being non empty set
for O being Ordinal holds ConsecutiveSet2 (A,(succ O)) = new_set2 (ConsecutiveSet2 (A,O))
proof end;

theorem Th16: :: LATTICE8:16
for A being non empty set
for O being Ordinal
for T being Sequence st O <> 0 & O is limit_ordinal & dom T = O & ( for O1 being Ordinal st O1 in O holds
T . O1 = ConsecutiveSet2 (A,O1) ) holds
ConsecutiveSet2 (A,O) = union (rng T)
proof end;

registration
let A be non empty set ;
let O be Ordinal;
cluster ConsecutiveSet2 (A,O) -> non empty ;
coherence
not ConsecutiveSet2 (A,O) is empty
proof end;
end;

theorem Th17: :: LATTICE8:17
for A being non empty set
for O being Ordinal holds A c= ConsecutiveSet2 (A,O)
proof end;

definition
let A be non empty set ;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let O be Ordinal;
assume A1: O in dom q ;
func Quadr2 (q,O) -> Element of [:(ConsecutiveSet2 (A,O)),(ConsecutiveSet2 (A,O)), the carrier of L, the carrier of L:] equals :Def6: :: LATTICE8:def 6
q . O;
correctness
coherence
q . O is Element of [:(ConsecutiveSet2 (A,O)),(ConsecutiveSet2 (A,O)), the carrier of L, the carrier of L:]
;
proof end;
end;

:: deftheorem Def6 defines Quadr2 LATTICE8:def 6 :
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being QuadrSeq of d
for O being Ordinal st O in dom q holds
Quadr2 (q,O) = q . O;

definition
let A be non empty set ;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let O be Ordinal;
func ConsecutiveDelta2 (q,O) -> set means :Def7: :: LATTICE8:def 7
ex L0 being Sequence st
( it = last L0 & dom L0 = succ O & L0 . 0 = d & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_bi_fun2 ((BiFun ((L0 . C),(ConsecutiveSet2 (A,C)),L)),(Quadr2 (q,C))) ) & ( for C being Ordinal st C in succ O & C <> 0 & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) );
correctness
existence
ex b1 being set ex L0 being Sequence st
( b1 = last L0 & dom L0 = succ O & L0 . 0 = d & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_bi_fun2 ((BiFun ((L0 . C),(ConsecutiveSet2 (A,C)),L)),(Quadr2 (q,C))) ) & ( for C being Ordinal st C in succ O & C <> 0 & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) )
;
uniqueness
for b1, b2 being set st ex L0 being Sequence st
( b1 = last L0 & dom L0 = succ O & L0 . 0 = d & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_bi_fun2 ((BiFun ((L0 . C),(ConsecutiveSet2 (A,C)),L)),(Quadr2 (q,C))) ) & ( for C being Ordinal st C in succ O & C <> 0 & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) ) & ex L0 being Sequence st
( b2 = last L0 & dom L0 = succ O & L0 . 0 = d & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_bi_fun2 ((BiFun ((L0 . C),(ConsecutiveSet2 (A,C)),L)),(Quadr2 (q,C))) ) & ( for C being Ordinal st C in succ O & C <> 0 & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def7 defines ConsecutiveDelta2 LATTICE8:def 7 :
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being QuadrSeq of d
for O being Ordinal
for b6 being set holds
( b6 = ConsecutiveDelta2 (q,O) iff ex L0 being Sequence st
( b6 = last L0 & dom L0 = succ O & L0 . 0 = d & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_bi_fun2 ((BiFun ((L0 . C),(ConsecutiveSet2 (A,C)),L)),(Quadr2 (q,C))) ) & ( for C being Ordinal st C in succ O & C <> 0 & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) ) );

theorem Th18: :: LATTICE8:18
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being QuadrSeq of d holds ConsecutiveDelta2 (q,0) = d
proof end;

theorem Th19: :: LATTICE8:19
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 (q,(succ O)) = new_bi_fun2 ((BiFun ((ConsecutiveDelta2 (q,O)),(ConsecutiveSet2 (A,O)),L)),(Quadr2 (q,O)))
proof end;

theorem Th20: :: LATTICE8:20
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being QuadrSeq of d
for T being Sequence
for O being Ordinal st O <> 0 & O is limit_ordinal & dom T = O & ( for O1 being Ordinal st O1 in O holds
T . O1 = ConsecutiveDelta2 (q,O1) ) holds
ConsecutiveDelta2 (q,O) = union (rng T)
proof end;

theorem Th21: :: LATTICE8:21
for A being non empty set
for O, O1, O2 being Ordinal st O1 c= O2 holds
ConsecutiveSet2 (A,O1) c= ConsecutiveSet2 (A,O2)
proof end;

theorem Th22: :: LATTICE8:22
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 (q,O) is BiFunction of (ConsecutiveSet2 (A,O)),L
proof end;

definition
let A be non empty set ;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let O be Ordinal;
:: original: ConsecutiveDelta2
redefine func ConsecutiveDelta2 (q,O) -> BiFunction of (ConsecutiveSet2 (A,O)),L;
coherence
ConsecutiveDelta2 (q,O) is BiFunction of (ConsecutiveSet2 (A,O)),L
by Th22;
end;

theorem Th23: :: LATTICE8:23
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being QuadrSeq of d
for O being Ordinal holds d c= ConsecutiveDelta2 (q,O)
proof end;

theorem Th24: :: LATTICE8:24
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for O1, O2 being Ordinal
for q being QuadrSeq of d st O1 c= O2 holds
ConsecutiveDelta2 (q,O1) c= ConsecutiveDelta2 (q,O2)
proof end;

theorem Th25: :: LATTICE8:25
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L st d is zeroed holds
for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 (q,O) is zeroed
proof end;

theorem Th26: :: LATTICE8:26
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L st d is symmetric holds
for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 (q,O) is symmetric
proof end;

theorem Th27: :: LATTICE8:27
for A being non empty set
for L being lower-bounded LATTICE st L is modular holds
for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds
for O being Ordinal
for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta2 (q,O) is u.t.i.
proof end;

theorem :: LATTICE8:28
for A being non empty set
for L being lower-bounded modular LATTICE
for d being distance_function of A,L
for O being Ordinal
for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta2 (q,O) is distance_function of (ConsecutiveSet2 (A,O)),L by ;

definition
let A be non empty set ;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
func NextSet2 d -> set equals :: LATTICE8:def 8
ConsecutiveSet2 (A,());
correctness
coherence
ConsecutiveSet2 (A,()) is set
;
;
end;

:: deftheorem defines NextSet2 LATTICE8:def 8 :
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L holds NextSet2 d = ConsecutiveSet2 (A,());

registration
let A be non empty set ;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
cluster NextSet2 d -> non empty ;
coherence
not NextSet2 d is empty
;
end;

definition
let A be non empty set ;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
func NextDelta2 q -> set equals :: LATTICE8:def 9
ConsecutiveDelta2 (q,());
correctness
coherence
ConsecutiveDelta2 (q,()) is set
;
;
end;

:: deftheorem defines NextDelta2 LATTICE8:def 9 :
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being QuadrSeq of d holds NextDelta2 q = ConsecutiveDelta2 (q,());

definition
let A be non empty set ;
let L be lower-bounded modular LATTICE;
let d be distance_function of A,L;
let q be QuadrSeq of d;
:: original: NextDelta2
redefine func NextDelta2 q -> distance_function of (),L;
coherence
NextDelta2 q is distance_function of (),L
by ;
end;

definition
let A be non empty set ;
let L be lower-bounded LATTICE;
let d be distance_function of A,L;
let Aq be non empty set ;
let dq be distance_function of Aq,L;
pred Aq,dq is_extension2_of A,d means :: LATTICE8:def 10
ex q being QuadrSeq of d st
( Aq = NextSet2 d & dq = NextDelta2 q );
end;

:: deftheorem defines is_extension2_of LATTICE8:def 10 :
for A being non empty set
for L being lower-bounded LATTICE
for d being distance_function of A,L
for Aq being non empty set
for dq being distance_function of Aq,L holds
( Aq,dq is_extension2_of A,d iff ex q being QuadrSeq of d st
( Aq = NextSet2 d & dq = NextDelta2 q ) );

theorem Th29: :: LATTICE8:29
for A being non empty set
for L being lower-bounded LATTICE
for d being distance_function of A,L
for Aq being non empty set
for dq being distance_function of Aq,L st Aq,dq is_extension2_of A,d holds
for x, y being Element of A
for a, b being Element of L st d . (x,y) <= a "\/" b holds
ex z1, z2 being Element of Aq st
( dq . (x,z1) = a & dq . (z1,z2) = ((d . (x,y)) "\/" a) "/\" b & dq . (z2,y) = a )
proof end;

definition
let A be non empty set ;
let L be lower-bounded modular LATTICE;
let d be distance_function of A,L;
mode ExtensionSeq2 of A,d -> Function means :Def11: :: LATTICE8:def 11
( dom it = NAT & it . 0 = [A,d] & ( for n being Nat ex A9 being non empty set ex d9 being distance_function of A9,L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension2_of A9,d9 & it . n = [A9,d9] & it . (n + 1) = [Aq,dq] ) ) );
existence
ex b1 being Function st
( dom b1 = NAT & b1 . 0 = [A,d] & ( for n being Nat ex A9 being non empty set ex d9 being distance_function of A9,L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension2_of A9,d9 & b1 . n = [A9,d9] & b1 . (n + 1) = [Aq,dq] ) ) )
proof end;
end;

:: deftheorem Def11 defines ExtensionSeq2 LATTICE8:def 11 :
for A being non empty set
for L being lower-bounded modular LATTICE
for d being distance_function of A,L
for b4 being Function holds
( b4 is ExtensionSeq2 of A,d iff ( dom b4 = NAT & b4 . 0 = [A,d] & ( for n being Nat ex A9 being non empty set ex d9 being distance_function of A9,L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension2_of A9,d9 & b4 . n = [A9,d9] & b4 . (n + 1) = [Aq,dq] ) ) ) );

theorem Th30: :: LATTICE8:30
for A being non empty set
for L being lower-bounded modular LATTICE
for d being distance_function of A,L
for S being ExtensionSeq2 of A,d
for k, l being Nat st k <= l holds
(S . k) 1 c= (S . l) 1
proof end;

theorem Th31: :: LATTICE8:31
for A being non empty set
for L being lower-bounded modular LATTICE
for d being distance_function of A,L
for S being ExtensionSeq2 of A,d
for k, l being Nat st k <= l holds
(S . k) 2 c= (S . l) 2
proof end;

theorem Th32: :: LATTICE8:32
for L being lower-bounded modular LATTICE
for S being ExtensionSeq2 of the carrier of L, BasicDF L
for FS being non empty set st FS = union { ((S . i) 1) where i is Element of NAT : verum } holds
union { ((S . i) 2) where i is Element of NAT : verum } is distance_function of FS,L
proof end;

theorem Th33: :: LATTICE8:33
for L being lower-bounded modular LATTICE
for S being ExtensionSeq2 of the carrier of L, BasicDF L
for FS being non empty set
for FD being distance_function of FS,L
for x, y being Element of FS
for a, b being Element of L st FS = union { ((S . i) 1) where i is Element of NAT : verum } & FD = union { ((S . i) 2) where i is Element of NAT : verum } & FD . (x,y) <= a "\/" b holds
ex z1, z2 being Element of FS st
( FD . (x,z1) = a & FD . (z1,z2) = ((FD . (x,y)) "\/" a) "/\" b & FD . (z2,y) = a )
proof end;

Lm3: for m being Element of NAT holds
( not m in Seg 4 or m = 1 or m = 2 or m = 3 or m = 4 )

proof end;

Lm4: for j being Nat st 1 <= j & j < 4 & not j = 1 & not j = 2 holds
j = 3

proof end;

theorem Th34: :: LATTICE8:34
for L being lower-bounded modular LATTICE
for S being ExtensionSeq2 of the carrier of L, BasicDF L
for FS being non empty set
for FD being distance_function of FS,L
for f being Homomorphism of L,()
for e1, e2 being Equivalence_Relation of FS
for x, y being object st f = alpha FD & FS = union { ((S . i) 1) where i is Element of NAT : verum } & FD = union { ((S . i) 2) where i is Element of NAT : verum } & e1 in the carrier of () & e2 in the carrier of () & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of FS st
( len F = 2 + 2 & x,y are_joint_by F,e1,e2 )
proof end;

theorem Th35: :: LATTICE8:35
for L being lower-bounded modular LATTICE holds L has_a_representation_of_type<= 2
proof end;

:: <=> :: L has_a_representation_of_type<= 2 iff L is modular
:: Jonsson Theorem for modular lattices
theorem :: LATTICE8:36
for L being lower-bounded LATTICE holds
( L has_a_representation_of_type<= 2 iff L is modular ) by ;