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 A1, TARSKI:def 1;

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 XBOOLE_1:45, XBOOLE_1:79;

the InternalRel of DP c= [:A,A:] \/ [:B,B:]

( 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 A11, XBOOLE_1:23;

then [#] DP is disconnected by A2;

hence DP is disconnected ; :: thesis: verum

given a, b being Element of DP such that A1: a <> b ; :: thesis: DP is disconnected

not b in {a} by A1, TARSKI:def 1;

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 XBOOLE_1:45, XBOOLE_1:79;

the InternalRel of DP c= [:A,A:] \/ [:B,B:]

proof

then A11:
the InternalRel of DP = the InternalRel of DP /\ ([:A,A:] \/ [:B,B:])
by XBOOLE_1:28;
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 A3, Def1;

then A6: x1 = x2 by A4, RELAT_1:def 10;

end;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 A3, Def1;

then A6: x1 = x2 by A4, RELAT_1:def 10;

per cases
( x1 in A or not x1 in A )
;

end;

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 A7, ZFMISC_1:87;

hence x in [:A,A:] \/ [:B,B:] by A4, A6, A8; :: thesis: verum

end;[x1,x1] in [:A,A:] by A7, ZFMISC_1:87;

hence x in [:A,A:] \/ [:B,B:] by A4, A6, A8; :: thesis: verum

suppose A9:
not x1 in A
; :: thesis: x in [:A,A:] \/ [:B,B:]

x1 in the carrier of DP
by A5, A4, RELAT_1:def 10;

then x1 in the carrier of DP \ A by A9, XBOOLE_0:def 5;

then x1 in the carrier of DP /\ B by XBOOLE_1:48;

then x1 in B by XBOOLE_1:28;

then A10: [x1,x1] in [:B,B:] by ZFMISC_1:87;

[:B,B:] c= [:A,A:] \/ [:B,B:] by XBOOLE_1:7;

hence x in [:A,A:] \/ [:B,B:] by A4, A6, A10; :: thesis: verum

end;then x1 in the carrier of DP \ A by A9, XBOOLE_0:def 5;

then x1 in the carrier of DP /\ B by XBOOLE_1:48;

then x1 in B by XBOOLE_1:28;

then A10: [x1,x1] in [:B,B:] by ZFMISC_1:87;

[:B,B:] c= [:A,A:] \/ [:B,B:] by XBOOLE_1:7;

hence x in [:A,A:] \/ [:B,B:] by A4, A6, A10; :: thesis: verum

( 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 A11, XBOOLE_1:23;

then [#] DP is disconnected by A2;

hence DP is disconnected ; :: thesis: verum