let X be set ; :: thesis: for F being Field_Subset of X
for A being Subset of X st A in F holds
A,({} X) followed_by ({} X) is Covering of A,F
let F be Field_Subset of X; :: thesis: for A being Subset of X st A in F holds
A,({} X) followed_by ({} X) is Covering of A,F
let A be Subset of X; :: thesis: ( A in F implies A,({} X) followed_by ({} X) is Covering of A,F )
assume C0: A in F ; :: thesis: A,({} X) followed_by ({} X) is Covering of A,F
reconsider Sets = A,({} X) followed_by ({} X) as SetSequence of X ;
C1: ( Sets . 0 = A & Sets . 1 = {} X ) by FUNCT_7:124, FUNCT_7:125;
for n being Nat holds Sets . n in F

proof

let n be Nat; :: thesis: Sets . n in F

per cases ( n = 0 or n = 1 or n > 1 ) by NAT_1:26;

suppose n = 0 ; :: thesis: Sets . n in F

hence Sets . n in F by C0, FUNCT_7:124; :: thesis: verum

end;

suppose n = 1 ; :: thesis: Sets . n in F

hence Sets . n in F by C1, PROB_1:10; :: thesis: verum

end;

suppose n > 1 ; :: thesis: Sets . n in F

then Sets . n = {} by FUNCT_7:126;
hence Sets . n in F by PROB_1:10; :: thesis: verum

end;

end;

end;

then reconsider Sets = Sets as Set_Sequence of F by DDef4;
A c= union (rng Sets)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in union (rng Sets) )
assume D1: x in A ; :: thesis: x in union (rng Sets)
dom Sets = NAT by FUNCT_2:def 1;
then Sets . 0 in rng Sets by FUNCT_1:12;
hence x in union (rng Sets) by C1, D1, TARSKI:def 4; :: thesis: verum

end;

hence A,({} X) followed_by ({} X) is Covering of A,F by Def2; :: thesis: verum