let a, b be object ; :: thesis: ( a <> b implies ( {[a,b],[b,a]} is irreflexive & {[a,b],[b,a]} is symmetric ) )
assume A0: a <> b ; :: thesis: ( {[a,b],[b,a]} is irreflexive & {[a,b],[b,a]} is symmetric )
reconsider R = {[a,b],[b,a]} as Relation ;
a1: for x, y being object st [x,y] in R holds
[y,x] in R
proof
let x, y be object ; :: thesis: ( [x,y] in R implies [y,x] in R )
assume [x,y] in R ; :: thesis: [y,x] in R
then ( [x,y] = [a,b] or [x,y] = [b,a] ) by TARSKI:def 2;
then ( ( x = a & y = b ) or ( x = b & y = a ) ) by XTUPLE_0:1;
hence [y,x] in R by TARSKI:def 2; :: thesis: verum
end;
for x being object st x in field R holds
not [x,x] in R
proof
let x be object ; :: thesis: ( x in field R implies not [x,x] in R )
assume ( x in field R & [x,x] in R ) ; :: thesis: contradiction
then ( [x,x] = [a,b] or [x,x] = [b,a] ) by TARSKI:def 2;
then ( ( x = a & x = b ) or ( x = b & x = a ) ) by XTUPLE_0:1;
hence contradiction by A0; :: thesis: verum
end;
hence ( {[a,b],[b,a]} is irreflexive & {[a,b],[b,a]} is symmetric ) by a1, RELAT_2:def 10, RELAT_2:def 2, LemSym; :: thesis: verum