let x be set ; :: thesis: RelIncl {x} = {[x,x]}
A1: field {[x,x]} = {x} by Th2;
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 ( Y in {x} & Z in {x} ) ; :: thesis: ( [Y,Z] in {[x,x]} iff Y c= Z )
then A2: ( Y = x & Z = x ) by TARSKI:def 1;
hence ( [Y,Z] in {[x,x]} implies Y c= Z ) ; :: thesis: ( Y c= Z implies [Y,Z] in {[x,x]} )
thus ( Y c= Z implies [Y,Z] in {[x,x]} ) by A2, TARSKI:def 1; :: thesis: verum

end;

hence RelIncl {x} = {[x,x]} by A1, WELLORD2:def 1; :: thesis: verum