let A be non empty Poset; :: thesis: for a1, a2 being Element of A
for S, T being Subset of A st a1 < a2 & a1 in S & a2 in T & T is Initial_Segm of S holds
a1 in T
let a1, a2 be Element of A; :: thesis: for S, T being Subset of A st a1 < a2 & a1 in S & a2 in T & T is Initial_Segm of S holds
a1 in T
let S, T be Subset of A; :: thesis: ( a1 < a2 & a1 in S & a2 in T & T is Initial_Segm of S implies a1 in T )
assume that
A1: a1 < a2 and
A2: a1 in S and
A3: a2 in T and
A4: T is Initial_Segm of S ; :: thesis: a1 in T
consider a being Element of A such that
a in S and
A5: T = InitSegm (S,a) by A2, A4, Def11;
now :: thesis: for b being Element of A st b in {a} holds
a1 < b
let b be Element of A; :: thesis: ( b in {a} implies a1 < b )
assume b in {a} ; :: thesis: a1 < b
then A6: b = a by TARSKI:def 1;
a2 in LowerCone {a} by A3, A5, XBOOLE_0:def 4;
then A7: ex a3 being Element of A st
( a3 = a2 & ( for c being Element of A st c in {a} holds
a3 < c ) ) ;
a in {a} by TARSKI:def 1;
then a2 < a by A7;
hence a1 < b by A1, A6, Th5; :: thesis: verum
end;
then a1 in LowerCone {a} ;
hence a1 in T by A2, A5, XBOOLE_0:def 4; :: thesis: verum