let DP be non empty discrete Poset; ( 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
; 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
let x be
object ;
TARSKI:def 3 ( not x in the InternalRel of DP or x in [:A,A:] \/ [:B,B:] )
assume A3:
x in the
InternalRel of
DP
;
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 )
;
suppose A7:
x1 in A
;
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;
verum end; suppose A9:
not
x1 in A
;
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;
verum 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 A11, XBOOLE_1:23;
then
[#] DP is disconnected
by A2;
hence
DP is disconnected
; verum