let A be non empty set ; :: thesis: for L being non empty Sublattice of EqRelLATT A holds
( L is trivial or ex e being Equivalence_Relation of A st
( e in the carrier of L & e <> id A ) )
let L be non empty Sublattice of EqRelLATT A; :: thesis: ( L is trivial or ex e being Equivalence_Relation of A st
( e in the carrier of L & e <> id A ) )
now :: thesis: ( ( for e being Equivalence_Relation of A holds
( not e in the carrier of L or not e <> id A ) ) implies L is trivial )
assume A1: for e being Equivalence_Relation of A holds
( not e in the carrier of L or not e <> id A ) ; :: thesis: L is trivial
thus L is trivial :: thesis: verum
proof
consider x being object such that
A2: x in the carrier of L by XBOOLE_0:def 1;
the carrier of L c= the carrier of (EqRelLATT A) by YELLOW_0:def 13;
then reconsider e = x as Equivalence_Relation of A by A2, LATTICE5:4;
the carrier of L = {x}
proof
thus the carrier of L c= {x} :: according to XBOOLE_0:def 10 :: thesis: {x} c= the carrier of L
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of L or a in {x} )
assume A3: a in the carrier of L ; :: thesis: a in {x}
the carrier of L c= the carrier of (EqRelLATT A) by YELLOW_0:def 13;
then reconsider B = a as Equivalence_Relation of A by A3, LATTICE5:4;
B = id A by A1, A3
.= e by A1, A2 ;
hence a in {x} by TARSKI:def 1; :: thesis: verum
end;
let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in {x} or A in the carrier of L )
assume A in {x} ; :: thesis: A in the carrier of L
hence A in the carrier of L by A2, TARSKI:def 1; :: thesis: verum
end;
hence L is trivial ; :: thesis: verum
end;
end;
hence ( L is trivial or ex e being Equivalence_Relation of A st
( e in the carrier of L & e <> id A ) ) ; :: thesis: verum