let I be set ; :: thesis: for X, x being ManySortedSet of st X is non-empty holds
( [|{x},X|] is non-empty & [|X,{x}|] is non-empty )
let X, x be ManySortedSet of ; :: thesis: ( X is non-empty implies ( [|{x},X|] is non-empty & [|X,{x}|] is non-empty ) )
assume A1: X is non-empty ; :: thesis: ( [|{x},X|] is non-empty & [|X,{x}|] is non-empty )
thus [|{x},X|] is non-empty :: thesis: [|X,{x}|] is non-empty

proof

let i be set ; :: according to PBOOLE:def 16 :: thesis: ( not i in I or not [|{x},X|] . i is empty )
assume A2: i in I ; :: thesis: not [|{x},X|] . i is empty
then not X . i is empty by A1, PBOOLE:def 16;
then not [:{(x . i)},(X . i):] is empty by ZFMISC_1:130;
then not [:({x} . i),(X . i):] is empty by A2, Def1;
hence not [|{x},X|] . i is empty by A2, PBOOLE:def 21; :: thesis: verum

end;

let i be set ; :: according to PBOOLE:def 16 :: thesis: ( not i in I or not [|X,{x}|] . i is empty )
assume A3: i in I ; :: thesis: not [|X,{x}|] . i is empty
then not X . i is empty by A1, PBOOLE:def 16;
then not [:(X . i),{(x . i)}:] is empty by ZFMISC_1:130;
then not [:(X . i),({x} . i):] is empty by A3, Def1;
hence not [|X,{x}|] . i is empty by A3, PBOOLE:def 21; :: thesis: verum