reconsider e1 = nabla A, e2 = id A as Element of (EqRelLATT A) by LATTICE5:4;
set a = the Element of A;
set b = the Element of A \ { the Element of A};
set Y = subrelstr {e1,e2};
A1: the carrier of (subrelstr {e1,e2}) = {e1,e2} by YELLOW_0:def 15;
e1 = [:A,A:] by EQREL_1:def 1;
then A2: e2 <= e1 by LATTICE5:6;
A3: for x, y being Element of (EqRelLATT A) st x in the carrier of (subrelstr {e1,e2}) & y in the carrier of (subrelstr {e1,e2}) & ex_inf_of {x,y}, EqRelLATT A holds
inf {x,y} in the carrier of (subrelstr {e1,e2})

proof

let x, y be Element of (EqRelLATT A); :: thesis:
assume that
A4: ( x in the carrier of (subrelstr {e1,e2}) & y in the carrier of (subrelstr {e1,e2}) ) and
ex_inf_of {x,y}, EqRelLATT A ; :: thesis:

per cases by A1, A4, TARSKI:def 2;

suppose ( x = e1 & y = e1 ) ; :: thesis:

then inf {x,y} = e1 "/\" e1 by YELLOW_0:40
.= e1 by YELLOW_5:2 ;
hence inf {x,y} in the carrier of (subrelstr {e1,e2}) by A1, TARSKI:def 2; :: thesis:

end;

suppose ( x = e1 & y = e2 ) ; :: thesis:

then inf {x,y} = e1 "/\" e2 by YELLOW_0:40
.= e2 by A2, YELLOW_5:10 ;
hence inf {x,y} in the carrier of (subrelstr {e1,e2}) by A1, TARSKI:def 2; :: thesis:

end;

suppose ( x = e2 & y = e1 ) ; :: thesis:

then inf {x,y} = e2 "/\" e1 by YELLOW_0:40
.= e2 by A2, YELLOW_5:10 ;
hence inf {x,y} in the carrier of (subrelstr {e1,e2}) by A1, TARSKI:def 2; :: thesis:

end;

suppose ( x = e2 & y = e2 ) ; :: thesis:

then inf {x,y} = e2 "/\" e2 by YELLOW_0:40
.= e2 by YELLOW_5:2 ;
hence inf {x,y} in the carrier of (subrelstr {e1,e2}) by A1, TARSKI:def 2; :: thesis:

end;

A5: subrelstr {e1,e2} is finitely_typed

proof

take A ; :: according to LATTICE8:def 1 :: thesis:
thus for e being object st e in the carrier of (subrelstr {e1,e2}) holds
e is Equivalence_Relation of A by A1, TARSKI:def 2; :: thesis:
take o = 3; :: thesis:
thus for eq1, eq2 being Equivalence_Relation of A
for x1, y1 being object st eq1 in the carrier of (subrelstr {e1,e2}) & eq2 in the carrier of (subrelstr {e1,e2}) & [x1,y1] in eq1 "\/" eq2 holds
ex F being non empty FinSequence of A st
( len F = o & x1,y1 are_joint_by F,eq1,eq2 ) :: thesis:

proof

let eq1, eq2 be Equivalence_Relation of A; :: thesis:
let x1, y1 be object ; :: thesis:
assume that
A6: eq1 in the carrier of (subrelstr {e1,e2}) and
A7: eq2 in the carrier of (subrelstr {e1,e2}) and
A8: [x1,y1] in eq1 "\/" eq2 ; :: thesis:
( eq1 = e2 or eq1 <> e2 ) ;
then consider z being object such that
A9: ( ( eq1 = e2 & z = x1 ) or ( eq1 <> e2 & z = y1 ) ) ;
ex x2, y2 being object st
( [x1,y1] = [x2,y2] & x2 in A & y2 in A ) by A8, RELSET_1:2;
then ( x1 in A & y1 in A ) by XTUPLE_0:1;
then reconsider F = <*x1,z,y1*> as non empty FinSequence of A by A9, FINSEQ_2:14;
take F ; :: thesis:

per cases by A9;

suppose A10: ( eq1 = e2 & z = x1 ) ; :: thesis:

then A11: F . 2 = x1 ;
A13: for i being Element of NAT st 1 <= i & i < len F holds
( ( i is odd implies [(F . i),(F . (i + 1))] in eq1 ) & ( i is even implies [(F . i),(F . (i + 1))] in eq2 ) )

proof

let i be Element of NAT ; :: thesis:
assume that
A14: 1 <= i and
A15: i < len F ; :: thesis:
i < 2 + 1 by A15, FINSEQ_1:45;
then i <= 2 by NAT_1:13;
then A16: not not i = 0 & ... & not i = 2 by NAT_1:60;

per cases by A1, A7, A10, A14, A16, Lm1, Lm2, TARSKI:def 2;

suppose A17: ( i = 1 & i is odd & eq1 = e2 & eq2 = e1 ) ; :: thesis:

ex x2, y2 being object st
( [x1,y1] = [x2,y2] & x2 in A & y2 in A ) by A8, RELSET_1:2;
then x1 in A by XTUPLE_0:1;
hence ( ( i is odd implies [(F . i),(F . (i + 1))] in eq1 ) & ( i is even implies [(F . i),(F . (i + 1))] in eq2 ) ) by A11, A17, EQREL_1:5; :: thesis:

end;

suppose A18: ( i = 1 & i is odd & eq1 = e2 & eq2 = e2 ) ; :: thesis:

end;

suppose A19: ( i = 2 & i is even & eq1 = e2 & eq2 = e1 ) ; :: thesis:

then eq1 "\/" eq2 = e2 "\/" e1 by LATTICE5:10
.= eq2 by A2, A19, YELLOW_5:8 ;
hence ( ( i is odd implies [(F . i),(F . (i + 1))] in eq1 ) & ( i is even implies [(F . i),(F . (i + 1))] in eq2 ) ) by A8, A11, A19; :: thesis:

end;

suppose ( i = 2 & i is even & eq1 = e2 & eq2 = e2 ) ; :: thesis:

hence ( ( i is odd implies [(F . i),(F . (i + 1))] in eq1 ) & ( i is even implies [(F . i),(F . (i + 1))] in eq2 ) ) by A8, A11; :: thesis:

end;

( len F = 3 & F . 3 = y1 ) by FINSEQ_1:45;
hence ( len F = o & x1,y1 are_joint_by F,eq1,eq2 ) by A13; :: thesis:

end;

suppose A20: ( eq1 <> e2 & z = y1 ) ; :: thesis:

then A21: F . 2 = y1 ;
A23: for i being Element of NAT st 1 <= i & i < len F holds
( ( i is odd implies [(F . i),(F . (i + 1))] in eq1 ) & ( i is even implies [(F . i),(F . (i + 1))] in eq2 ) )

proof

let i be Element of NAT ; :: thesis:
assume that
A24: 1 <= i and
A25: i < len F ; :: thesis:
i < 2 + 1 by A25, FINSEQ_1:45;
then i <= 2 by NAT_1:13;
then A26: not not i = 0 & ... & not i = 2 by NAT_1:60;

per cases by A1, A6, A7, A20, A24, A26, Lm1, Lm2, TARSKI:def 2;

suppose ( i = 1 & i is odd & eq1 = e1 & eq2 = e1 ) ; :: thesis:

hence ( ( i is odd implies [(F . i),(F . (i + 1))] in eq1 ) & ( i is even implies [(F . i),(F . (i + 1))] in eq2 ) ) by A8, A21; :: thesis:

end;

suppose A27: ( i = 1 & i is odd & eq1 = e1 & eq2 = e2 ) ; :: thesis:

then eq1 "\/" eq2 = e1 "\/" e2 by LATTICE5:10
.= eq1 by A2, A27, YELLOW_5:8 ;
hence ( ( i is odd implies [(F . i),(F . (i + 1))] in eq1 ) & ( i is even implies [(F . i),(F . (i + 1))] in eq2 ) ) by A8, A21, A27; :: thesis:

end;

suppose A28: ( i = 2 & i is even & eq1 = e1 & eq2 = e1 ) ; :: thesis:

ex x2, y2 being object st
( [x1,y1] = [x2,y2] & x2 in A & y2 in A ) by A8, RELSET_1:2;
then y1 in A by XTUPLE_0:1;
hence ( ( i is odd implies [(F . i),(F . (i + 1))] in eq1 ) & ( i is even implies [(F . i),(F . (i + 1))] in eq2 ) ) by A21, A28, EQREL_1:5; :: thesis:

end;

suppose A29: ( i = 2 & i is even & eq1 = e1 & eq2 = e2 ) ; :: thesis:

end;

( len F = 3 & F . 1 = x1 ) by FINSEQ_1:45;
hence ( len F = o & x1,y1 are_joint_by F,eq1,eq2 ) by A23; :: thesis:

end;

A30: for x, y being Element of (EqRelLATT A) st x in the carrier of (subrelstr {e1,e2}) & y in the carrier of (subrelstr {e1,e2}) & ex_sup_of {x,y}, EqRelLATT A holds
sup {x,y} in the carrier of (subrelstr {e1,e2})

proof

let x, y be Element of (EqRelLATT A); :: thesis:
assume that
A31: ( x in the carrier of (subrelstr {e1,e2}) & y in the carrier of (subrelstr {e1,e2}) ) and
ex_sup_of {x,y}, EqRelLATT A ; :: thesis:

per cases by A1, A31, TARSKI:def 2;

suppose ( x = e1 & y = e1 ) ; :: thesis:

then sup {x,y} = e1 "\/" e1 by YELLOW_0:41
.= e1 by YELLOW_5:1 ;
hence sup {x,y} in the carrier of (subrelstr {e1,e2}) by A1, TARSKI:def 2; :: thesis:

end;

suppose ( x = e1 & y = e2 ) ; :: thesis:

then sup {x,y} = e1 "\/" e2 by YELLOW_0:41
.= e1 by A2, YELLOW_5:8 ;
hence sup {x,y} in the carrier of (subrelstr {e1,e2}) by A1, TARSKI:def 2; :: thesis:

end;

suppose ( x = e2 & y = e1 ) ; :: thesis:

then sup {x,y} = e2 "\/" e1 by YELLOW_0:41
.= e1 by A2, YELLOW_5:8 ;
hence sup {x,y} in the carrier of (subrelstr {e1,e2}) by A1, TARSKI:def 2; :: thesis:

end;

suppose ( x = e2 & y = e2 ) ; :: thesis:

then sup {x,y} = e2 "\/" e2 by YELLOW_0:41
.= e2 by YELLOW_5:1 ;
hence sup {x,y} in the carrier of (subrelstr {e1,e2}) by A1, TARSKI:def 2; :: thesis:

end;

A32: the Element of A <> the Element of A \ { the Element of A} by ZFMISC_1:56;
A33: not subrelstr {e1,e2} is trivial

proof

assume subrelstr {e1,e2} is trivial ; :: thesis:
then ex s being Element of (subrelstr {e1,e2}) st the carrier of (subrelstr {e1,e2}) = {s} by TEX_1:def 1;
then nabla A = id A by A1, ZFMISC_1:5;
then [:A,A:] = id A by EQREL_1:def 1;
then [ the Element of A, the Element of A \ { the Element of A}] in id A by ZFMISC_1:def 2;
hence contradiction by A32, RELAT_1:def 10; :: thesis:

end;

reconsider Y = subrelstr {e1,e2} as non empty full Sublattice of EqRelLATT A by A3, A30, YELLOW_0:def 16, YELLOW_0:def 17;
take Y ; :: thesis:
thus ( not Y is trivial & Y is finitely_typed & Y is full ) by A33, A5; :: thesis: