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 set ; :: 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 consider j being set such that
A2: ( j in J & j in dom A & a in A . j ) by Def1;
thus a in union A,K by A1, A2, Def1; :: thesis: verum

end;