let X be set ; :: thesis: for IT being Subset-Family of X holds

( IT is non-increasing-closed iff for A1 being SetSequence of X st A1 is V74() & rng A1 c= IT holds

lim A1 in IT )

let IT be Subset-Family of X; :: thesis: ( IT is non-increasing-closed iff for A1 being SetSequence of X st A1 is V74() & rng A1 c= IT holds

lim A1 in IT )

thus ( IT is non-increasing-closed implies for A1 being SetSequence of X st A1 is V74() & rng A1 c= IT holds

lim A1 in IT ) :: thesis: ( ( for A1 being SetSequence of X st A1 is V74() & rng A1 c= IT holds

lim A1 in IT ) implies IT is non-increasing-closed )

lim A1 in IT ; :: thesis: IT is non-increasing-closed

for A1 being SetSequence of X st A1 is V74() & rng A1 c= IT holds

Intersection A1 in IT

( IT is non-increasing-closed iff for A1 being SetSequence of X st A1 is V74() & rng A1 c= IT holds

lim A1 in IT )

let IT be Subset-Family of X; :: thesis: ( IT is non-increasing-closed iff for A1 being SetSequence of X st A1 is V74() & rng A1 c= IT holds

lim A1 in IT )

thus ( IT is non-increasing-closed implies for A1 being SetSequence of X st A1 is V74() & rng A1 c= IT holds

lim A1 in IT ) :: thesis: ( ( for A1 being SetSequence of X st A1 is V74() & rng A1 c= IT holds

lim A1 in IT ) implies IT is non-increasing-closed )

proof

assume A4:
for A1 being SetSequence of X st A1 is V74() & rng A1 c= IT holds
assume A1:
IT is non-increasing-closed
; :: thesis: for A1 being SetSequence of X st A1 is V74() & rng A1 c= IT holds

lim A1 in IT

lim A1 in IT ; :: thesis: verum

end;lim A1 in IT

now :: thesis: for A1 being SetSequence of X st A1 is V74() & rng A1 c= IT holds

lim A1 in IT

hence
for A1 being SetSequence of X st A1 is V74() & rng A1 c= IT holds lim A1 in IT

let A1 be SetSequence of X; :: thesis: ( A1 is V74() & rng A1 c= IT implies lim A1 in IT )

assume that

A2: A1 is V74() and

A3: rng A1 c= IT ; :: thesis: lim A1 in IT

Intersection A1 in IT by A1, A2, A3;

hence lim A1 in IT by A2, SETLIM_1:64; :: thesis: verum

end;assume that

A2: A1 is V74() and

A3: rng A1 c= IT ; :: thesis: lim A1 in IT

Intersection A1 in IT by A1, A2, A3;

hence lim A1 in IT by A2, SETLIM_1:64; :: thesis: verum

lim A1 in IT ; :: thesis: verum

lim A1 in IT ; :: thesis: IT is non-increasing-closed

for A1 being SetSequence of X st A1 is V74() & rng A1 c= IT holds

Intersection A1 in IT

proof

hence
IT is non-increasing-closed
; :: thesis: verum
let A1 be SetSequence of X; :: thesis: ( A1 is V74() & rng A1 c= IT implies Intersection A1 in IT )

assume that

A5: A1 is V74() and

A6: rng A1 c= IT ; :: thesis: Intersection A1 in IT

lim A1 in IT by A4, A5, A6;

hence Intersection A1 in IT by A5, SETLIM_1:64; :: thesis: verum

end;assume that

A5: A1 is V74() and

A6: rng A1 c= IT ; :: thesis: Intersection A1 in IT

lim A1 in IT by A4, A5, A6;

hence Intersection A1 in IT by A5, SETLIM_1:64; :: thesis: verum