scheme :: ORDERS_5:sch 2
RelStrMin{ F1() -> transitive connected RelStr , F2() -> finite Subset of F1(), P1[ Element of F1()] } :
ex x being Element of F1() st
( x in F2() & P1[x] & ( for y being Element of F1() st y in F2() & y <~ x holds
not P1[y] ) )
provided
A1: ex x being Element of F1() st
( x in F2() & P1[x] )