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 Def7;
then the InternalRel of A is_strongly_connected_in S by A1;
hence S is Chain of A by Def7; :: thesis: verum