let x be object ; :: thesis: 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 ; :: thesis: ( 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} ; :: thesis: ( [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; :: thesis: ( 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; :: thesis: verum

end;

field {[x,x]} = {x} by RELAT_1:173;
hence RelIncl {x} = {[x,x]} by A1, Def1; :: thesis: verum