let R be RelStr ; :: thesis: for C being Clique of R
for S being Subset of C holds S is Clique of R
let C be Clique of R; :: thesis: for S being Subset of C holds S is Clique of R
let S be Subset of C; :: thesis: S is Clique of R
set iR = the InternalRel of R;
A1: the InternalRel of R is_connected_in C by Def1;
the InternalRel of R is_connected_in S by A1;
hence S is Clique of R by Def1, XBOOLE_1:1; :: thesis: verum