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