let X be set ; :: thesis: for A1, A2, A3 being SetSequence of X st ( for n being Nat holds A3 . n = (A1 . n) \/ (A2 . n) ) holds
for n being Nat holds ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence A3) . n
let A1, A2, A3 be SetSequence of X; :: thesis: ( ( for n being Nat holds A3 . n = (A1 . n) \/ (A2 . n) ) implies for n being Nat holds ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence A3) . n )
assume A1: for n being Nat holds A3 . n = (A1 . n) \/ (A2 . n) ; :: thesis: for n being Nat holds ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence A3) . n
let n be Nat; :: thesis: ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence A3) . n
set X1 = inferior_setsequence A1;
set X2 = inferior_setsequence A2;
set X3 = inferior_setsequence A3;

now :: thesis: for x being object st x in ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) holds
x in (inferior_setsequence A3) . n

let x be object ; :: thesis: ( x in ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) implies b₁ in (inferior_setsequence A3) . n )
assume A2: x in ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) ; :: thesis: b₁ in (inferior_setsequence A3) . n

per cases ( x in (inferior_setsequence A1) . n or x in (inferior_setsequence A2) . n ) by A2, XBOOLE_0:def 3;

suppose A3: x in (inferior_setsequence A1) . n ; :: thesis: b₁ in (inferior_setsequence A3) . n

now :: thesis: for k being Nat holds x in A3 . (n + k)

let k be Nat; :: thesis: x in A3 . (n + k)
( x in A1 . (n + k) & A3 . (n + k) = (A1 . (n + k)) \/ (A2 . (n + k)) ) by A1, A3, Th19;
hence x in A3 . (n + k) by XBOOLE_0:def 3; :: thesis: verum

end;

hence x in (inferior_setsequence A3) . n by Th19; :: thesis: verum

end;

suppose A4: x in (inferior_setsequence A2) . n ; :: thesis: b₁ in (inferior_setsequence A3) . n

now :: thesis: for k being Nat holds x in A3 . (n + k)

let k be Nat; :: thesis: x in A3 . (n + k)
( x in A2 . (n + k) & A3 . (n + k) = (A1 . (n + k)) \/ (A2 . (n + k)) ) by A1, A4, Th19;
hence x in A3 . (n + k) by XBOOLE_0:def 3; :: thesis: verum

end;

hence x in (inferior_setsequence A3) . n by Th19; :: thesis: verum

end;

end;

end;

hence ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence A3) . n ; :: thesis: verum