let X be set ; :: thesis: for p being FinSequence of bool X holds { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } is Subset-Family of X

let p be FinSequence of bool X; :: thesis: { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } is Subset-Family of X

{ (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } c= bool X

let p be FinSequence of bool X; :: thesis: { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } is Subset-Family of X

{ (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } c= bool X

proof

hence
{ (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } is Subset-Family of X
; :: thesis: verum
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } or z in bool X )

assume z in { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } ; :: thesis: z in bool X

then ex q being FinSequence of BOOLEAN st

( z = Intersect (rng (MergeSequence (p,q))) & len q = len p ) ;

hence z in bool X ; :: thesis: verum

end;assume z in { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } ; :: thesis: z in bool X

then ex q being FinSequence of BOOLEAN st

( z = Intersect (rng (MergeSequence (p,q))) & len q = len p ) ;

hence z in bool X ; :: thesis: verum