let A be non empty Poset; :: thesis: for a1, a2 being Element of A
for S being Subset of A st a1 < a2 holds
InitSegm (S,a1) c= InitSegm (S,a2)
let a1, a2 be Element of A; :: thesis: for S being Subset of A st a1 < a2 holds
InitSegm (S,a1) c= InitSegm (S,a2)
let S be Subset of A; :: thesis: ( a1 < a2 implies InitSegm (S,a1) c= InitSegm (S,a2) )
assume A1: a1 < a2 ; :: thesis: InitSegm (S,a1) c= InitSegm (S,a2)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in InitSegm (S,a1) or x in InitSegm (S,a2) )
assume A2: x in InitSegm (S,a1) ; :: thesis: x in InitSegm (S,a2)
then x in LowerCone {a1} by XBOOLE_0:def 4;
then consider a being Element of A such that
A3: a = x and
A4: for b being Element of A st b in {a1} holds
a < b ;
a1 in {a1} by TARSKI:def 1;
then a < a1 by A4;
then a < a2 by A1, Th5;
then for b being Element of A st b in {a2} holds
a < b by TARSKI:def 1;
then A5: x in LowerCone {a2} by A3;
x in S by A2, XBOOLE_0:def 4;
hence x in InitSegm (S,a2) by A5, XBOOLE_0:def 4; :: thesis: verum