let X be non empty set ; :: thesis:
let Y be Sublattice of EqRelLATT X; :: thesis:
let n be Element of NAT ; :: thesis:
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 set 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:
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 13;
((n + 1) + m) + 1 = (n + m) + 2 ;
then consider e1, e2 being Equivalence_Relation of X, x, y being set 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;
consider F1 being non empty FinSequence of X such that
A7: ( len F1 = n + 2 & x,y are_joint_by F1,e1,e2 ) by A2, A5;
( field e1 = X & field e2 = X ) by EQREL_1:16;
then A8: ( e1 is_reflexive_in X & e2 is_reflexive_in X ) by RELAT_2:def 9;
(n + 2) + m = (n + m) + 2 ;
then n + 2 <= (n + m) + 2 by NAT_1:11;
hence contradiction by A6, A7, A8, Th14; :: thesis: