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 )

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

A1: for Y, Z being set st Y in {x} & Z in {x} holds

( [Y,Z] in {[x,x]} iff Y c= Z )

proof

field {[x,x]} = {x}
by RELAT_1:173;
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;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

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