let C be non empty Poset; :: thesis: for x, s being set st x c= s & s in symplexes C holds

x in symplexes C

let x, s be set ; :: thesis: ( x c= s & s in symplexes C implies x in symplexes C )

assume that

A1: x c= s and

A2: s in symplexes C ; :: thesis: x in symplexes C

consider s1 being Element of Fin the carrier of C such that

A3: s1 = s and

A4: the InternalRel of C linearly_orders s1 by A2;

s1 c= the carrier of C by FINSUB_1:def 5;

then x c= the carrier of C by A1, A3;

then reconsider x1 = x as Element of Fin the carrier of C by A1, A2, FINSUB_1:def 5;

the InternalRel of C linearly_orders x by A1, A3, A4, ORDERS_1:38;

then x1 in { A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A } ;

hence x in symplexes C ; :: thesis: verum

x in symplexes C

let x, s be set ; :: thesis: ( x c= s & s in symplexes C implies x in symplexes C )

assume that

A1: x c= s and

A2: s in symplexes C ; :: thesis: x in symplexes C

consider s1 being Element of Fin the carrier of C such that

A3: s1 = s and

A4: the InternalRel of C linearly_orders s1 by A2;

s1 c= the carrier of C by FINSUB_1:def 5;

then x c= the carrier of C by A1, A3;

then reconsider x1 = x as Element of Fin the carrier of C by A1, A2, FINSUB_1:def 5;

the InternalRel of C linearly_orders x by A1, A3, A4, ORDERS_1:38;

then x1 in { A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A } ;

hence x in symplexes C ; :: thesis: verum