let A be RelStr ; :: thesis: for C being Chain of A
for S being Subset of A st S c= C holds
S is Chain of A
let C be Chain of A; :: thesis: for S being Subset of A st S c= C holds
S is Chain of A
let S be Subset of A; :: thesis: ( S c= C implies S is Chain of A )
assume A1: S c= C ; :: thesis: S is Chain of A
the InternalRel of A is_strongly_connected_in C by Def11;
then the InternalRel of A is_strongly_connected_in S by A1, ORDERS_1:96;
hence S is Chain of A by Def11; :: thesis: verum