consider a being Element of A;
consider b being Element of A \ {a};
A1: ( b in A & a <> b ) by ZFMISC_1:64;
reconsider e1 = nabla A, e2 = id A as Element of (EqRelLATT A) by LATTICE5:4;
set Y = subrelstr {e1,e2};
A2: the carrier of (subrelstr {e1,e2}) = {e1,e2} by YELLOW_0:def 15;
e1 = [:A,A:] by EQREL_1:def 1;
then A3: e2 <= e1 by LATTICE5:6;
A4: subrelstr {e1,e2} is meet-inheriting

proof

thus 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}) :: according to YELLOW_0:def 16 :: thesis:

proof

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

per cases by A2, A5, 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 A2, TARSKI:def 2; :: thesis:

end;

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

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

end;

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

then inf {x,y} = e2 "/\" e1 by YELLOW_0:40
.= e2 by A3, YELLOW_5:10 ;
hence inf {x,y} in the carrier of (subrelstr {e1,e2}) by A2, 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 A2, TARSKI:def 2; :: thesis:

end;

thus verum ; :: thesis:

end;

A6: subrelstr {e1,e2} is join-inheriting

proof

thus 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}) :: according to YELLOW_0:def 17 :: thesis:

proof

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

per cases by A2, A7, 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 A2, TARSKI:def 2; :: thesis:

end;

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

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

end;

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

then sup {x,y} = e2 "\/" e1 by YELLOW_0:41
.= e1 by A3, YELLOW_5:8 ;
hence sup {x,y} in the carrier of (subrelstr {e1,e2}) by A2, 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 A2, TARSKI:def 2; :: thesis:

end;

thus verum ; :: thesis:

end;

A8: not subrelstr {e1,e2} is trivial

proof

assume subrelstr {e1,e2} is trivial ; :: thesis:
then consider s being Element of (subrelstr {e1,e2}) such that
A9: the carrier of (subrelstr {e1,e2}) = {s} by TEX_1:def 1;
nabla A = id A by A2, A9, ZFMISC_1:9;
then [:A,A:] = id A by EQREL_1:def 1;
then [a,b] in id A by ZFMISC_1:def 2;
hence contradiction by A1, RELAT_1:def 10; :: thesis:

end;

A10: subrelstr {e1,e2} is finitely_typed

proof

take A ; :: according to LATTICE8:def 2 :: thesis:
thus for e being set st e in the carrier of (subrelstr {e1,e2}) holds
e is Equivalence_Relation of A by A2, TARSKI:def 2; :: thesis:
take o = 3; :: thesis:
thus for eq1, eq2 being Equivalence_Relation of A
for x1, y1 being set 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 set ; :: thesis:
assume A11: ( eq1 in the carrier of (subrelstr {e1,e2}) & eq2 in the carrier of (subrelstr {e1,e2}) & [x1,y1] in eq1 "\/" eq2 ) ; :: thesis:
( eq1 = e2 or eq1 <> e2 ) ;
then consider z being set such that
A12: ( ( eq1 = e2 & z = x1 ) or ( eq1 <> e2 & z = y1 ) ) ;
consider x2, y2 being set such that
A13: ( [x1,y1] = [x2,y2] & x2 in A & y2 in A ) by A11, RELSET_1:6;
( x1 in A & y1 in A ) by A13, ZFMISC_1:33;
then reconsider F = <*x1,z,y1*> as non empty FinSequence of A by A12, FINSEQ_2:16;
take F ; :: thesis:

per cases by A12;

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

then A15: ( eq1 = e2 & len F = 3 & F . 1 = x1 & F . 2 = x1 & F . 3 = y1 ) by FINSEQ_1:62;
for i being Element of NAT st 1 <= i & i < len F holds
( ( not i is even 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 A16: ( 1 <= i & i < len F ) ; :: thesis:
then i < 2 + 1 by FINSEQ_1:62;
then i <= 2 by NAT_1:13;
then A17: ( i = 0 or i = 1 or i = 2 ) by NAT_1:27;

per cases by A2, A11, A14, A16, A17, Lm1, Lm2, TARSKI:def 2;

suppose A18: ( i = 1 & not i is even & eq1 = e2 & eq2 = e1 ) ; :: thesis:

consider x2, y2 being set such that
A19: ( [x1,y1] = [x2,y2] & x2 in A & y2 in A ) by A11, RELSET_1:6;
x1 in A by A19, ZFMISC_1:33;
hence ( ( not i is even implies [(F . i),(F . (i + 1))] in eq1 ) & ( i is even implies [(F . i),(F . (i + 1))] in eq2 ) ) by A15, A18, EQREL_1:11; :: thesis:

end;

suppose A20: ( i = 1 & not i is even & eq1 = e2 & eq2 = e2 ) ; :: thesis:

consider x2, y2 being set such that
A21: ( [x1,y1] = [x2,y2] & x2 in A & y2 in A ) by A11, RELSET_1:6;
x1 in A by A21, ZFMISC_1:33;
hence ( ( not i is even implies [(F . i),(F . (i + 1))] in eq1 ) & ( i is even implies [(F . i),(F . (i + 1))] in eq2 ) ) by A15, A20, EQREL_1:11; :: thesis:

end;

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

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

end;

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

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

end;

hence ( len F = o & x1,y1 are_joint_by F,eq1,eq2 ) by A15, LATTICE5:def 3; :: thesis:

end;

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

then A24: ( eq1 <> e2 & len F = 3 & F . 1 = x1 & F . 2 = y1 & F . 3 = y1 ) by FINSEQ_1:62;
for i being Element of NAT st 1 <= i & i < len F holds
( ( not i is even 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 A25: ( 1 <= i & i < len F ) ; :: thesis:
then i < 2 + 1 by FINSEQ_1:62;
then i <= 2 by NAT_1:13;
then A26: ( i = 0 or i = 1 or i = 2 ) by NAT_1:27;

per cases by A2, A11, A23, A25, A26, Lm1, Lm2, TARSKI:def 2;

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

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

end;

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

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

end;

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

consider x2, y2 being set such that
A29: ( [x1,y1] = [x2,y2] & x2 in A & y2 in A ) by A11, RELSET_1:6;
y1 in A by A29, ZFMISC_1:33;
hence ( ( not i is even implies [(F . i),(F . (i + 1))] in eq1 ) & ( i is even implies [(F . i),(F . (i + 1))] in eq2 ) ) by A24, A28, EQREL_1:11; :: thesis:

end;

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

consider x2, y2 being set such that
A31: ( [x1,y1] = [x2,y2] & x2 in A & y2 in A ) by A11, RELSET_1:6;
y1 in A by A31, ZFMISC_1:33;
hence ( ( not i is even implies [(F . i),(F . (i + 1))] in eq1 ) & ( i is even implies [(F . i),(F . (i + 1))] in eq2 ) ) by A24, A30, EQREL_1:11; :: thesis:

end;

hence ( len F = o & x1,y1 are_joint_by F,eq1,eq2 ) by A24, LATTICE5:def 3; :: thesis:

end;

reconsider Y = subrelstr {e1,e2} as non empty full Sublattice of EqRelLATT A by A4, A6;
take Y ; :: thesis:
thus ( not Y is trivial & Y is finitely_typed & Y is full ) by A8, A10; :: thesis: