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

proof

let x1, x2 be set ; :: according to RELAT_2:def 6 :: thesis: ( not x1 in S or not x2 in S or x1 = x2 or [x1,x2] in the InternalRel of R or [x2,x1] in the InternalRel of R )
assume ( x1 in S & x2 in S & x1 <> x2 ) ; :: thesis: ( [x1,x2] in the InternalRel of R or [x2,x1] in the InternalRel of R )
hence ( [x1,x2] in the InternalRel of R or [x2,x1] in the InternalRel of R ) by A1, RELAT_2:def 6; :: thesis: verum

end;

hence S is Clique of R by Def1, XBOOLE_1:1; :: thesis: verum