let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma st ASeq is V77() holds

for n, m being Nat st n < m holds

(Partial_Union ASeq) . n misses ASeq . m

let Sigma be SigmaField of Omega; :: thesis: for ASeq being SetSequence of Sigma st ASeq is V77() holds

for n, m being Nat st n < m holds

(Partial_Union ASeq) . n misses ASeq . m

let ASeq be SetSequence of Sigma; :: thesis: ( ASeq is V77() implies for n, m being Nat st n < m holds

(Partial_Union ASeq) . n misses ASeq . m )

assume A1: ASeq is V77() ; :: thesis: for n, m being Nat st n < m holds

(Partial_Union ASeq) . n misses ASeq . m

let n, m be Nat; :: thesis: ( n < m implies (Partial_Union ASeq) . n misses ASeq . m )

assume A2: n < m ; :: thesis: (Partial_Union ASeq) . n misses ASeq . m

assume (Partial_Union ASeq) . n meets ASeq . m ; :: thesis: contradiction

then consider x being object such that

A3: x in (Partial_Union ASeq) . n and

A4: x in ASeq . m by XBOOLE_0:3;

reconsider ASeq = ASeq as SetSequence of Omega ;

consider k being Nat such that

A5: k <= n and

A6: x in ASeq . k by A3, Th13;

ASeq . k misses ASeq . m by A1, A2, A5;

then (ASeq . k) /\ (ASeq . m) = {} ;

hence contradiction by A4, A6, XBOOLE_0:def 4; :: thesis: verum

for ASeq being SetSequence of Sigma st ASeq is V77() holds

for n, m being Nat st n < m holds

(Partial_Union ASeq) . n misses ASeq . m

let Sigma be SigmaField of Omega; :: thesis: for ASeq being SetSequence of Sigma st ASeq is V77() holds

for n, m being Nat st n < m holds

(Partial_Union ASeq) . n misses ASeq . m

let ASeq be SetSequence of Sigma; :: thesis: ( ASeq is V77() implies for n, m being Nat st n < m holds

(Partial_Union ASeq) . n misses ASeq . m )

assume A1: ASeq is V77() ; :: thesis: for n, m being Nat st n < m holds

(Partial_Union ASeq) . n misses ASeq . m

let n, m be Nat; :: thesis: ( n < m implies (Partial_Union ASeq) . n misses ASeq . m )

assume A2: n < m ; :: thesis: (Partial_Union ASeq) . n misses ASeq . m

assume (Partial_Union ASeq) . n meets ASeq . m ; :: thesis: contradiction

then consider x being object such that

A3: x in (Partial_Union ASeq) . n and

A4: x in ASeq . m by XBOOLE_0:3;

reconsider ASeq = ASeq as SetSequence of Omega ;

consider k being Nat such that

A5: k <= n and

A6: x in ASeq . k by A3, Th13;

ASeq . k misses ASeq . m by A1, A2, A5;

then (ASeq . k) /\ (ASeq . m) = {} ;

hence contradiction by A4, A6, XBOOLE_0:def 4; :: thesis: verum