let X be set ; :: thesis: for B being SetSequence of X
for f being Function st dom f = NAT & ( for n being Element of NAT holds f . n = meet { (B . k) where k is Element of NAT : n <= k } ) holds
f is SetSequence of X
let B be SetSequence of X; :: thesis: for f being Function st dom f = NAT & ( for n being Element of NAT holds f . n = meet { (B . k) where k is Element of NAT : n <= k } ) holds
f is SetSequence of X
let f be Function; :: thesis: ( dom f = NAT & ( for n being Element of NAT holds f . n = meet { (B . k) where k is Element of NAT : n <= k } ) implies f is SetSequence of X )
assume that
A1: dom f = NAT and
A2: for n being Element of NAT holds f . n = meet { (B . k) where k is Element of NAT : n <= k } ; :: thesis: f is SetSequence of X
rng f c= bool X

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng f or z in bool X )
assume z in rng f ; :: thesis: z in bool X
then consider x being set such that
A3: x in dom f and
A4: z = f . x by FUNCT_1:def 3;
reconsider n = x as Element of NAT by A1, A3;
set Y = { (B . k) where k is Element of NAT : n <= k } ;
set y = meet { (B . k) where k is Element of NAT : n <= k } ;
A5: meet { (B . k) where k is Element of NAT : n <= k } is Subset of X

proof

A6: now

assume { (B . k) where k is Element of NAT : n <= k } <> {} ; :: thesis: meet { (B . k) where k is Element of NAT : n <= k } is Subset of X
then consider Z1 being set such that
A7: Z1 in { (B . k) where k is Element of NAT : n <= k } by XBOOLE_0:def 1;
A8: ex k1 being Element of NAT st
( Z1 = B . k1 & n <= k1 ) by A7;

now

let x be set ; :: thesis: ( x in meet { (B . k) where k is Element of NAT : n <= k } implies x in X )
assume x in meet { (B . k) where k is Element of NAT : n <= k } ; :: thesis: x in X
then x in Z1 by A7, SETFAM_1:def 1;
hence x in X by A8; :: thesis: verum

end;

hence meet { (B . k) where k is Element of NAT : n <= k } is Subset of X by TARSKI:def 3; :: thesis: verum

end;

now

assume { (B . k) where k is Element of NAT : n <= k } = {} ; :: thesis: meet { (B . k) where k is Element of NAT : n <= k } is Subset of X
then meet { (B . k) where k is Element of NAT : n <= k } = {} by SETFAM_1:def 1;
hence meet { (B . k) where k is Element of NAT : n <= k } is Subset of X by XBOOLE_1:2; :: thesis: verum

end;

hence meet { (B . k) where k is Element of NAT : n <= k } is Subset of X by A6; :: thesis: verum

end;

z = meet { (B . k) where k is Element of NAT : n <= k } by A2, A4;
hence z in bool X by A5; :: thesis: verum

end;

hence f is SetSequence of X by A1, FUNCT_2:2; :: thesis: verum