set R = CompleteRelStr n;
set cR = the carrier of (CompleteRelStr n);
set iR = the InternalRel of (CompleteRelStr n);
A1:
the carrier of (CompleteRelStr n) = n
by Def7;
thus
CompleteRelStr n is irreflexive
by A1, Th32; CompleteRelStr n is symmetric
thus
CompleteRelStr n is symmetric
verumproof
let x,
y be
object ;
RELAT_2:def 3,
NECKLACE:def 3 ( not x in the carrier of (CompleteRelStr n) or not y in the carrier of (CompleteRelStr n) or not [x,y] in the InternalRel of (CompleteRelStr n) or [y,x] in the InternalRel of (CompleteRelStr n) )
assume
(
x in the
carrier of
(CompleteRelStr n) &
y in the
carrier of
(CompleteRelStr n) )
;
( not [x,y] in the InternalRel of (CompleteRelStr n) or [y,x] in the InternalRel of (CompleteRelStr n) )
then A2:
(
x in n &
y in n )
by Def7;
assume
[x,y] in the
InternalRel of
(CompleteRelStr n)
;
[y,x] in the InternalRel of (CompleteRelStr n)
hence
[y,x] in the
InternalRel of
(CompleteRelStr n)
by A2, Th32;
verum
end;