let A be non empty Poset; for S, T being Subset of A st S <> {} & S is Initial_Segm of T holds
not T is Initial_Segm of S
let S, T be Subset of A; ( S <> {} & S is Initial_Segm of T implies not T is Initial_Segm of S )
assume that
A1:
S <> {}
and
A2:
S is Initial_Segm of T
and
A3:
T is Initial_Segm of S
; contradiction
now contradictionper cases
( S = {} or T = {} or ( S <> {} & T <> {} ) )
;
suppose
S = {}
;
contradictionhence
contradiction
by A1;
verum end; suppose A4:
(
S <> {} &
T <> {} )
;
contradictionthen consider a2 being
Element of
A such that A5:
a2 in T
and A6:
S = InitSegm (
T,
a2)
by A2, Def11;
consider a1 being
Element of
A such that A7:
a1 in S
and A8:
T = InitSegm (
S,
a1)
by A3, A4, Def11;
a1 in LowerCone {a2}
by A7, A6, XBOOLE_0:def 4;
then A9:
ex
a being
Element of
A st
(
a = a1 & ( for
b being
Element of
A st
b in {a2} holds
a < b ) )
;
a2 in LowerCone {a1}
by A8, A5, XBOOLE_0:def 4;
then A10:
ex
a3 being
Element of
A st
(
a3 = a2 & ( for
b being
Element of
A st
b in {a1} holds
a3 < b ) )
;
a1 in {a1}
by TARSKI:def 1;
then A11:
a2 < a1
by A10;
a2 in {a2}
by TARSKI:def 1;
then
a1 < a2
by A9;
hence
contradiction
by A11, Th4;
verum end;
hence
contradiction
; verum