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 object ; :: 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;
then x . i in (X . i) \/ (Y . i) by XBOOLE_0:def 3;
hence x . i in (X (\/) Y) . i by A2, Def4; :: thesis: verum