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

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