let F be finite set ; :: thesis: for A being FinSequence of bool F
for J, K being set st J c= K holds
union (A,J) c= union (A,K)
let A be FinSequence of bool F; :: thesis: for J, K being set st J c= K holds
union (A,J) c= union (A,K)
let J, K be set ; :: thesis: ( J c= K implies union (A,J) c= union (A,K) )
assume A1: J c= K ; :: thesis: union (A,J) c= union (A,K)
thus union (A,J) c= union (A,K) :: thesis: verum

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union (A,J) or a in union (A,K) )
assume a in union (A,J) ; :: thesis: a in union (A,K)
then ex j being set st
( j in J & j in dom A & a in A . j ) by Def1;
hence a in union (A,K) by A1, Def1; :: thesis: verum

end;