let I be set ; for x, y, X being ManySortedSet of I holds
( ( x in X & y in X ) iff {x,y} (/\) X = {x,y} )
let x, y, X be ManySortedSet of I; ( ( x in X & y in X ) iff {x,y} (/\) X = {x,y} )
thus
( x in X & y in X implies {x,y} (/\) X = {x,y} )
( {x,y} (/\) X = {x,y} implies ( x in X & y in X ) )proof
assume that A1:
x in X
and A2:
y in X
;
{x,y} (/\) X = {x,y}
now for i being object st i in I holds
({x,y} (/\) X) . i = {x,y} . ilet i be
object ;
( i in I implies ({x,y} (/\) X) . i = {x,y} . i )assume A3:
i in I
;
({x,y} (/\) X) . i = {x,y} . ithen A4:
x . i in X . i
by A1;
A5:
y . i in X . i
by A2, A3;
thus ({x,y} (/\) X) . i =
({x,y} . i) /\ (X . i)
by A3, PBOOLE:def 5
.=
{(x . i),(y . i)} /\ (X . i)
by A3, Def2
.=
{(x . i),(y . i)}
by A4, A5, ZFMISC_1:47
.=
{x,y} . i
by A3, Def2
;
verum end;
hence
{x,y} (/\) X = {x,y}
;
verum
end;
assume A6:
{x,y} (/\) X = {x,y}
; ( x in X & y in X )
thus
x in X
y in X
let i be object ; PBOOLE:def 1 ( not i in I or y . i in X . i )
assume A8:
i in I
; y . i in X . i
then {(x . i),(y . i)} /\ (X . i) =
({x,y} . i) /\ (X . i)
by Def2
.=
({x,y} (/\) X) . i
by A8, PBOOLE:def 5
.=
{(x . i),(y . i)}
by A6, A8, Def2
;
hence
y . i in X . i
by ZFMISC_1:55; verum