let R be RelStr ; :: thesis: for S being Subset of R holds
( S is Clique of R iff for a, b being Element of R st a in S & b in S & a <> b & not a <= b holds
b <= a )
let S be Subset of R; :: thesis: ( S is Clique of R iff for a, b being Element of R st a in S & b in S & a <> b & not a <= b holds
b <= a )
set RR = the InternalRel of R;

hereby :: thesis: ( ( for a, b being Element of R st a in S & b in S & a <> b & not a <= b holds
b <= a ) implies S is Clique of R )

assume S is Clique of R ; :: thesis: for a, b being Element of R st a in S & b in S & a <> b & not a <= b holds
b <= a
then A1: the InternalRel of R is_connected_in S by Def1;
let a, b be Element of R; :: thesis: ( a in S & b in S & a <> b & not a <= b implies b <= a )
assume ( a in S & b in S & a <> b ) ; :: thesis: ( a <= b or b <= a )
then ( [a,b] in the InternalRel of R or [b,a] in the InternalRel of R ) by A1;
hence ( a <= b or b <= a ) ; :: thesis: verum

end;

assume A2: for a, b being Element of R st a in S & b in S & a <> b & not a <= b holds
b <= a ; :: thesis: S is Clique of R
the InternalRel of R is_connected_in S

proof

let x, y be object ; :: according to RELAT_2:def 6 :: thesis: ( not x in S or not y in S or x = y or [x,y] in the InternalRel of R or [y,x] in the InternalRel of R )
assume A3: ( x in S & y in S & x <> y ) ; :: thesis: ( [x,y] in the InternalRel of R or [y,x] in the InternalRel of R )
then reconsider x9 = x, y9 = y as Element of R ;
( x9 <= y9 or y9 <= x9 ) by A3, A2;
hence ( [x,y] in the InternalRel of R or [y,x] in the InternalRel of R ) ; :: thesis: verum

end;

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