let X be non empty trivial 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 set such that
A1: X = {x} by REALSET1:def 4;
let a, b be set ; :: 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 A2: ( a in X & b in X & [a,b] in R ) ; :: thesis: [b,a] in R
then ( a = x & b = x ) by A1, TARSKI:def 1;
hence [b,a] in R by A2; :: thesis: verum