let X be non empty set ; :: thesis: for Y being Sublattice of EqRelLATT X

for n being Element of NAT st ex e being Equivalence_Relation of X st

( e in the carrier of Y & e <> id X ) & ( for e1, e2 being Equivalence_Relation of X

for x, y being object st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds

ex F being non empty FinSequence of X st

( len F = n + 2 & x,y are_joint_by F,e1,e2 ) ) holds

type_of Y <= n

let Y be Sublattice of EqRelLATT X; :: thesis: for n being Element of NAT st ex e being Equivalence_Relation of X st

( e in the carrier of Y & e <> id X ) & ( for e1, e2 being Equivalence_Relation of X

for x, y being object st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds

ex F being non empty FinSequence of X st

( len F = n + 2 & x,y are_joint_by F,e1,e2 ) ) holds

type_of Y <= n

let n be Element of NAT ; :: thesis: ( ex e being Equivalence_Relation of X st

( e in the carrier of Y & e <> id X ) & ( for e1, e2 being Equivalence_Relation of X

for x, y being object st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds

ex F being non empty FinSequence of X st

( len F = n + 2 & x,y are_joint_by F,e1,e2 ) ) implies type_of Y <= n )

assume that

A1: ex e being Equivalence_Relation of X st

( e in the carrier of Y & e <> id X ) and

A2: for e1, e2 being Equivalence_Relation of X

for x, y being object st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds

ex F being non empty FinSequence of X st

( len F = n + 2 & x,y are_joint_by F,e1,e2 ) and

A3: n < type_of Y ; :: thesis: contradiction

n + 1 <= type_of Y by A3, NAT_1:13;

then consider m being Nat such that

A4: type_of Y = (n + 1) + m by NAT_1:10;

reconsider m = m as Element of NAT by ORDINAL1:def 12;

((n + 1) + m) + 1 = (n + m) + 2 ;

then consider e1, e2 being Equivalence_Relation of X, x, y being object such that

A5: ( e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 ) and

A6: for F being non empty FinSequence of X holds

( not len F = (n + m) + 2 or not x,y are_joint_by F,e1,e2 ) by A1, A4, Def4;

A7: (n + 2) + m = (n + m) + 2 ;

field e2 = X by EQREL_1:9;

then A8: e2 is_reflexive_in X by RELAT_2:def 9;

field e1 = X by EQREL_1:9;

then A9: e1 is_reflexive_in X by RELAT_2:def 9;

ex F1 being non empty FinSequence of X st

( len F1 = n + 2 & x,y are_joint_by F1,e1,e2 ) by A2, A5;

hence contradiction by A6, A9, A8, A7, Th12, NAT_1:11; :: thesis: verum

for n being Element of NAT st ex e being Equivalence_Relation of X st

( e in the carrier of Y & e <> id X ) & ( for e1, e2 being Equivalence_Relation of X

for x, y being object st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds

ex F being non empty FinSequence of X st

( len F = n + 2 & x,y are_joint_by F,e1,e2 ) ) holds

type_of Y <= n

let Y be Sublattice of EqRelLATT X; :: thesis: for n being Element of NAT st ex e being Equivalence_Relation of X st

( e in the carrier of Y & e <> id X ) & ( for e1, e2 being Equivalence_Relation of X

for x, y being object st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds

ex F being non empty FinSequence of X st

( len F = n + 2 & x,y are_joint_by F,e1,e2 ) ) holds

type_of Y <= n

let n be Element of NAT ; :: thesis: ( ex e being Equivalence_Relation of X st

( e in the carrier of Y & e <> id X ) & ( for e1, e2 being Equivalence_Relation of X

for x, y being object st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds

ex F being non empty FinSequence of X st

( len F = n + 2 & x,y are_joint_by F,e1,e2 ) ) implies type_of Y <= n )

assume that

A1: ex e being Equivalence_Relation of X st

( e in the carrier of Y & e <> id X ) and

A2: for e1, e2 being Equivalence_Relation of X

for x, y being object st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds

ex F being non empty FinSequence of X st

( len F = n + 2 & x,y are_joint_by F,e1,e2 ) and

A3: n < type_of Y ; :: thesis: contradiction

n + 1 <= type_of Y by A3, NAT_1:13;

then consider m being Nat such that

A4: type_of Y = (n + 1) + m by NAT_1:10;

reconsider m = m as Element of NAT by ORDINAL1:def 12;

((n + 1) + m) + 1 = (n + m) + 2 ;

then consider e1, e2 being Equivalence_Relation of X, x, y being object such that

A5: ( e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 ) and

A6: for F being non empty FinSequence of X holds

( not len F = (n + m) + 2 or not x,y are_joint_by F,e1,e2 ) by A1, A4, Def4;

A7: (n + 2) + m = (n + m) + 2 ;

field e2 = X by EQREL_1:9;

then A8: e2 is_reflexive_in X by RELAT_2:def 9;

field e1 = X by EQREL_1:9;

then A9: e1 is_reflexive_in X by RELAT_2:def 9;

ex F1 being non empty FinSequence of X st

( len F1 = n + 2 & x,y are_joint_by F1,e1,e2 ) by A2, A5;

hence contradiction by A6, A9, A8, A7, Th12, NAT_1:11; :: thesis: verum