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