let A be non trivial set ; :: thesis:
let L be non empty full finitely_typed Sublattice of EqRelLATT A; :: thesis:
let e be Equivalence_Relation of A; :: thesis:
assume that
A1: e in the carrier of L and
A2: e <> id A ; :: thesis:
assume A3: type_of L <= 2 ; :: thesis:
let a, b, c be Element of L; :: according to YELLOW11:def 3 :: thesis:
A4: the carrier of L c= the carrier of (EqRelLATT A) by YELLOW_0:def 13;
A5: b in the carrier of L ;
then reconsider b9 = b as Equivalence_Relation of A by A4, LATTICE5:4;
reconsider b99 = b9 as Element of (EqRelLATT A) by A4, A5;
A6: a in the carrier of L ;
then reconsider a9 = a as Equivalence_Relation of A by A4, LATTICE5:4;
A7: c in the carrier of L ;
then reconsider c9 = c as Equivalence_Relation of A by A4, LATTICE5:4;
reconsider c99 = c9 as Element of (EqRelLATT A) by A4, A7;
reconsider a99 = a9 as Element of (EqRelLATT A) by A4, A6;
A8: (a99 "\/" b99) "/\" c99 = (a99 "\/" b99) /\ c9 by LATTICE5:8
.= (a9 "\/" b9) /\ c9 by LATTICE5:10 ;
assume A9: a <= c ; :: thesis:
then a99 <= c99 by YELLOW_0:59;
then A10: a9 c= c9 by LATTICE5:6;
A11: a99 "\/" (b99 "/\" c99) <= (a99 "\/" b99) "/\" c99 by A9, YELLOW11:8, YELLOW_0:59;
A12: b9 /\ c9 = b99 "/\" c99 by LATTICE5:8;
then a9 "\/" (b9 /\ c9) = a99 "\/" (b99 "/\" c99) by LATTICE5:10;
then A13: a9 "\/" (b9 /\ c9) c= (a9 "\/" b9) /\ c9 by A11, A8, LATTICE5:6;
consider AA being non empty set such that
A14: for e being set st e in the carrier of L holds
e is Equivalence_Relation of AA and
A15: ex i being Element of NAT st
for e1, e2 being Equivalence_Relation of AA
for x, y being set 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 AA st
( len F = i & x,y are_joint_by F,e1,e2 ) by Def2;
e is Equivalence_Relation of AA by A1, A14;
then A16: ( field e = A & field e = AA ) by EQREL_1:9;
A17: (a9 "\/" b9) /\ c9 c= a9 "\/" (b9 /\ c9)

proof

let x, y be Element of A; :: according to RELSET_1:def 1 :: thesis:
assume A18: [x,y] in (a9 "\/" b9) /\ c9 ; :: thesis:
then A19: [x,y] in a9 "\/" b9 by XBOOLE_0:def 4;
A20: [x,y] in c9 by A18, XBOOLE_0:def 4;

per cases by A3, NAT_1:26;

suppose type_of L = 2 ; :: thesis:

then consider F being non empty FinSequence of A such that
A21: len F = 2 + 2 and
A22: x,y are_joint_by F,a9,b9 by A1, A2, A15, A16, A19, LATTICE5:def 4;
A23: F . 4 = y by A21, A22, LATTICE5:def 3;
consider l being Element of NAT such that
A24: l = 1 ;
(2 * l) + 1 = 3 by A24;
then A25: [(F . 3),(F . (3 + 1))] in a9 by A21, A22, LATTICE5:def 3;
consider k being Element of NAT such that
A26: k = 1 ;
2 * k = 2 by A26;
then A27: [(F . 2),(F . (2 + 1))] in b9 by A21, A22, LATTICE5:def 3;
A28: F . 1 = x by A22, LATTICE5:def 3;
reconsider BC = b9 /\ c9 as Element of (EqRelLATT A) by A12;
set z1 = F . 2;
set z2 = F . 3;
consider j being Element of NAT such that
A29: j = 0 ;
(2 * j) + 1 = 1 by A29;
then A30: [(F . 1),(F . (1 + 1))] in a9 by A21, A22, LATTICE5:def 3;
A31: a9 "\/" (b9 /\ c9) = a99 "\/" BC by LATTICE5:10;
BC <= BC "\/" a99 by YELLOW_0:22;
then A32: b9 /\ c9 c= a9 "\/" (b9 /\ c9) by A31, LATTICE5:6;
a99 <= a99 "\/" BC by YELLOW_0:22;
then A33: a9 c= a9 "\/" (b9 /\ c9) by A31, LATTICE5:6;
[y,x] in c9 by A20, EQREL_1:6;
then [(F . 3),x] in c9 by A10, A23, A25, EQREL_1:7;
then [(F . 3),(F . 2)] in c9 by A10, A28, A30, EQREL_1:7;
then [(F . 2),(F . 3)] in c9 by EQREL_1:6;
then [(F . 2),(F . 3)] in b9 /\ c9 by A27, XBOOLE_0:def 4;
then [x,(F . 3)] in a9 "\/" (b9 /\ c9) by A28, A30, A33, A32, EQREL_1:7;
hence [x,y] in a9 "\/" (b9 /\ c9) by A23, A25, A33, EQREL_1:7; :: thesis:

end;

suppose type_of L = 1 ; :: thesis:

then consider F being non empty FinSequence of A such that
A34: len F = 1 + 2 and
A35: x,y are_joint_by F,a9,b9 by A1, A2, A15, A16, A19, LATTICE5:def 4;
set z1 = F . 2;
consider k being Element of NAT such that
A36: k = 1 ;
reconsider BC = b9 /\ c9 as Element of (EqRelLATT A) by A12;
consider j being Element of NAT such that
A37: j = 0 ;
(2 * j) + 1 = 1 by A37;
then A38: [(F . 1),(F . (1 + 1))] in a9 by A34, A35, LATTICE5:def 3;
2 * k = 2 by A36;
then A39: [(F . 2),(F . (2 + 1))] in b9 by A34, A35, LATTICE5:def 3;
A40: a9 "\/" (b9 /\ c9) = a99 "\/" BC by LATTICE5:10;
A41: [x,y] in c9 by A18, XBOOLE_0:def 4;
A42: F . 1 = x by A35, LATTICE5:def 3;
then [(F . 2),x] in c9 by A10, A38, EQREL_1:6;
then A43: [(F . 2),y] in c9 by A41, EQREL_1:7;
BC <= BC "\/" a99 by YELLOW_0:22;
then A44: b9 /\ c9 c= a9 "\/" (b9 /\ c9) by A40, LATTICE5:6;
a99 <= a99 "\/" BC by YELLOW_0:22;
then A45: a9 c= a9 "\/" (b9 /\ c9) by A40, LATTICE5:6;
F . 3 = y by A34, A35, LATTICE5:def 3;
then [(F . 2),y] in b9 /\ c9 by A39, A43, XBOOLE_0:def 4;
hence [x,y] in a9 "\/" (b9 /\ c9) by A42, A38, A45, A44, EQREL_1:7; :: thesis:

end;

suppose type_of L = 0 ; :: thesis:

then consider F being non empty FinSequence of A such that
A46: ( len F = 0 + 2 & x,y are_joint_by F,a9,b9 ) by A1, A2, A15, A16, A19, LATTICE5:def 4;
reconsider BC = b9 /\ c9 as Element of (EqRelLATT A) by A12;
consider j being Element of NAT such that
A47: j = 0 ;
(2 * j) + 1 = 1 by A47;
then A48: [(F . 1),(F . (1 + 1))] in a9 by A46, LATTICE5:def 3;
( a99 <= a99 "\/" BC & a9 "\/" (b9 /\ c9) = a99 "\/" BC ) by LATTICE5:10, YELLOW_0:22;
then A49: a9 c= a9 "\/" (b9 /\ c9) by LATTICE5:6;
( F . 1 = x & F . 2 = y ) by A46, LATTICE5:def 3;
hence [x,y] in a9 "\/" (b9 /\ c9) by A48, A49; :: thesis:

end;

a99 "\/" b99 = a "\/" b by YELLOW_0:70;
then A50: (a "\/" b) "/\" c = (a99 "\/" b99) "/\" c99 by YELLOW_0:69
.= (a99 "\/" b99) /\ c9 by LATTICE5:8
.= (a9 "\/" b9) /\ c9 by LATTICE5:10 ;
A51: b99 "/\" c99 = b "/\" c by YELLOW_0:69;
a9 "\/" (b9 /\ c9) = a99 "\/" (b99 "/\" c99) by A12, LATTICE5:10
.= a "\/" (b "/\" c) by A51, YELLOW_0:70 ;
hence a "\/" (b "/\" c) = (a "\/" b) "/\" c by A13, A17, A50, XBOOLE_0:def 10; :: thesis: