let I be set ; :: thesis: for x, X, Y being ManySortedSet of I st ( x in X or x in Y ) holds
x in X \/ Y
let x, X, Y be ManySortedSet of I; :: thesis: ( ( x in X or x in Y ) implies x in X \/ Y )
assume A1: ( x in X or x in Y ) ; :: thesis: x in X \/ Y
let i be set ; :: according to PBOOLE:def 1 :: thesis: ( i in I implies x . i in (X \/ Y) . i )
assume A2: i in I ; :: thesis: x . i in (X \/ Y) . i
then ( x . i in X . i or x . i in Y . i ) by A1, Def4;
then x . i in (X . i) \/ (Y . i) by XBOOLE_0:def 3;
hence x . i in (X \/ Y) . i by A2, Def7; :: thesis: verum