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

proof

let x, y be Element of A; :: according to RELSET_1:def 1 :: thesis:
assume A15: [x,y] in (a9 "\/" b9) /\ c9 ; :: thesis:
then A16: [x,y] in a9 "\/" b9 by XBOOLE_0:def 4;
A17: [x,y] in c9 by A15, XBOOLE_0:def 4;
not not type_of L = 0 & ... & not type_of L = 2 by A3, NAT_1:60;

per cases ;

suppose type_of L = 2 ; :: thesis:

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

end;

suppose type_of L = 1 ; :: thesis:

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

end;

suppose type_of L = 0 ; :: thesis:

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

end;

a99 "\/" b99 = a "\/" b by YELLOW_0:70;
then A47: (a "\/" b) "/\" c = (a99 "\/" b99) "/\" c99 by YELLOW_0:69
.= (a99 "\/" b99) /\ c9 by LATTICE5:8
.= (a9 "\/" b9) /\ c9 by LATTICE5:10 ;
A48: b99 "/\" c99 = b "/\" c by YELLOW_0:69;
a9 "\/" (b9 /\ c9) = a99 "\/" (b99 "/\" c99) by A9, LATTICE5:10
.= a "\/" (b "/\" c) by A48, YELLOW_0:70 ;
hence a "\/" (b "/\" c) = (a "\/" b) "/\" c by A10, A14, A47; :: thesis: