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 )
reconsider Sets = (A,({} X)) followed_by ({} X) as SetSequence of X ;
A1: Sets . 0 = A by FUNCT_7:122;
A2: Sets . 1 = {} X by FUNCT_7:123;
assume A3: A in F ; :: thesis: (A,({} X)) followed_by ({} X) is Covering of A,F
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:25;

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

hence Sets . n in F by A3, FUNCT_7:122; :: thesis: verum

end;

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

hence Sets . n in F by A2, PROB_1:4; :: thesis: verum

end;

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

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

end;

end;

end;

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

proof

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

end;

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