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
A2:
the carrier of DP = (the carrier of DP \ {a}) \/ {a}
by XBOOLE_1:45;
A3:
the carrier of DP \ {a} misses {a}
by XBOOLE_1:79;
reconsider B = {a} as non empty Subset of DP ;
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;
A4:
the InternalRel of DP |_2 A = the InternalRel of DP /\ [:A,A:]
by WELLORD1:def 6;
A5:
the InternalRel of DP |_2 B = the InternalRel of DP /\ [:B,B:]
by WELLORD1:def 6;
the InternalRel of DP c= [:A,A:] \/ [:B,B:]
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in the InternalRel of DP or x in [:A,A:] \/ [:B,B:] )
assume A6:
x in the
InternalRel of
DP
;
:: thesis: x in [:A,A:] \/ [:B,B:]
then A7:
x in id the
carrier of
DP
by Def1;
consider x1,
x2 being
set such that A8:
x = [x1,x2]
by A6, RELAT_1:def 1;
A9:
x1 = x2
by A7, A8, RELAT_1:def 10;
per cases
( x1 in A or not x1 in A )
;
suppose A11:
not
x1 in A
;
:: thesis: x in [:A,A:] \/ [:B,B:]
x1 in the
carrier of
DP
by A7, A8, RELAT_1:def 10;
then
x1 in the
carrier of
DP \ A
by A11, 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 A12:
[x1,x1] in [:B,B:]
by ZFMISC_1:106;
[:B,B:] c= [:A,A:] \/ [:B,B:]
by XBOOLE_1:7;
hence
x in [:A,A:] \/ [:B,B:]
by A8, A9, A12;
:: thesis: verum end;
end;
then
the InternalRel of DP = the InternalRel of DP /\ ([:A,A:] \/ [:B,B:])
by XBOOLE_1:28;
then A13:
the InternalRel of DP = (the InternalRel of DP |_2 A) \/ (the InternalRel of DP |_2 B)
by A4, A5, XBOOLE_1:23;
[#] DP is disconnected
by A2, A3, A13, Def2;
hence
DP is disconnected
by Def3; :: thesis: verum