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 A1: ( x c= s & s in symplexes C ) ; :: thesis: x in symplexes C
then consider s1 being Element of Fin the carrier of C such that
A2: ( s1 = s & the InternalRel of C linearly_orders s1 ) ;
A3: the InternalRel of C linearly_orders x by A1, A2, ORDERS_1:134;
( s1 c= the carrier of C & s1 is finite ) by FINSUB_1:def 5;
then ( x c= the carrier of C & x is finite ) by A1, A2, XBOOLE_1:1;
then reconsider x1 = x as Element of Fin the carrier of C by FINSUB_1:def 5;
x1 in { A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A } by A3;
hence x in symplexes C ; :: thesis: verum