let n be Nat; :: thesis: for X being set
for A1 being SetSequence of X holds (Partial_Diff_Union A1) . n c= A1 . n
let X be set ; :: thesis: for A1 being SetSequence of X holds (Partial_Diff_Union A1) . n c= A1 . n
let A1 be SetSequence of X; :: thesis: (Partial_Diff_Union A1) . n c= A1 . n
for x being set st x in (Partial_Diff_Union A1) . n holds
x in A1 . n by Th19;
hence (Partial_Diff_Union A1) . n c= A1 . n by TARSKI:def 3; :: thesis: verum