let DP be non empty discrete Poset; :: thesis: ( ex a, b being Element of DP st a <> b implies DP is disconnected )
given a, b being Element of DP such that A1: a <> b ; :: thesis: DP is disconnected
not b in {a} by ;
then reconsider A = the carrier of DP \ {a} as non empty Subset of DP by XBOOLE_0:def 5;
reconsider B = {a} as non empty Subset of DP ;
A2: ( the carrier of DP = ( the carrier of DP \ {a}) \/ {a} & the carrier of DP \ {a} misses {a} ) by ;
the InternalRel of DP c= [:A,A:] \/ [:B,B:]
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the InternalRel of DP or x in [:A,A:] \/ [:B,B:] )
assume A3: x in the InternalRel of DP ; :: thesis: x in [:A,A:] \/ [:B,B:]
then consider x1, x2 being object such that
A4: x = [x1,x2] by RELAT_1:def 1;
A5: x in id the carrier of DP by ;
then A6: x1 = x2 by ;
per cases ( x1 in A or not x1 in A ) ;
suppose A7: x1 in A ; :: thesis: x in [:A,A:] \/ [:B,B:]
A8: [:A,A:] c= [:A,A:] \/ [:B,B:] by XBOOLE_1:7;
[x1,x1] in [:A,A:] by ;
hence x in [:A,A:] \/ [:B,B:] by A4, A6, A8; :: thesis: verum
end;
end;
end;
then A11: the InternalRel of DP = the InternalRel of DP /\ ([:A,A:] \/ [:B,B:]) by XBOOLE_1:28;
( the InternalRel of DP |_2 A = the InternalRel of DP /\ [:A,A:] & the InternalRel of DP |_2 B = the InternalRel of DP /\ [:B,B:] ) by WELLORD1:def 6;
then the InternalRel of DP = ( the InternalRel of DP |_2 A) \/ ( the InternalRel of DP |_2 B) by ;
then [#] DP is disconnected by A2;
hence DP is disconnected ; :: thesis: verum