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 ; :: thesis: verum
end;
suppose n = 1 ; :: thesis: Sets . n in F
hence Sets . n in F by ; :: 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 ; :: thesis: verum
end;
hence (A,({} X)) followed_by ({} X) is Covering of A,F by Def3; :: thesis: verum