let X be 1 -element set ; :: thesis: for R being Relation of X holds R is_symmetric_in X
let R be Relation of X; :: thesis: R is_symmetric_in X
consider x being object such that
A1: X = {x} by ZFMISC_1:131;
let a, b be object ; :: according to RELAT_2:def 3 :: thesis: ( not a in X or not b in X or not [a,b] in R or [b,a] in R )
assume that
A2: a in X and
A3: ( b in X & [a,b] in R ) ; :: thesis: [b,a] in R
a = x by A1, A2, TARSKI:def 1;
hence [b,a] in R by A1, A3, TARSKI:def 1; :: thesis: verum