let I be set ; for x, X being ManySortedSet of I st X is V2() holds
( [|{x},X|] is V2() & [|X,{x}|] is V2() )
let x, X be ManySortedSet of I; ( X is V2() implies ( [|{x},X|] is V2() & [|X,{x}|] is V2() ) )
assume A1:
X is V2()
; ( [|{x},X|] is V2() & [|X,{x}|] is V2() )
thus
[|{x},X|] is V2()
[|X,{x}|] is V2()
let i be object ; PBOOLE:def 13 ( not i in I or not [|X,{x}|] . i is empty )
assume A3:
i in I
; not [|X,{x}|] . i is empty
then
not X . i is empty
by A1;
then
not [:(X . i),{(x . i)}:] is empty
by ZFMISC_1:107;
then
not [:(X . i),({x} . i):] is empty
by A3, Def1;
hence
not [|X,{x}|] . i is empty
by A3, PBOOLE:def 16; verum