let x be object ; RelIncl {x} = {[x,x]}
A1:
for Y, Z being set st Y in {x} & Z in {x} holds
( [Y,Z] in {[x,x]} iff Y c= Z )
proof
let Y,
Z be
set ;
( Y in {x} & Z in {x} implies ( [Y,Z] in {[x,x]} iff Y c= Z ) )
assume that A2:
Y in {x}
and A3:
Z in {x}
;
( [Y,Z] in {[x,x]} iff Y c= Z )
A4:
Y = x
by A2, TARSKI:def 1;
hence
(
[Y,Z] in {[x,x]} implies
Y c= Z )
by A3, TARSKI:def 1;
( Y c= Z implies [Y,Z] in {[x,x]} )
Z = x
by A3, TARSKI:def 1;
hence
(
Y c= Z implies
[Y,Z] in {[x,x]} )
by A4, TARSKI:def 1;
verum
end;
field {[x,x]} = {x}
by RELAT_1:173;
hence
RelIncl {x} = {[x,x]}
by A1, Def1; verum