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 set ; :: 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, Th29;
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