let X be set ; :: thesis: union { V where V is finite Subset of X : card V <= 2 } = X
set G = { V where V is finite Subset of X : card V <= 2 } ;
thus union { V where V is finite Subset of X : card V <= 2 } c= X :: according to XBOOLE_0:def 10 :: thesis: X c= union { V where V is finite Subset of X : card V <= 2 }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union { V where V is finite Subset of X : card V <= 2 } or x in X )
assume x in union { V where V is finite Subset of X : card V <= 2 } ; :: thesis: x in X
then consider a being set such that
Ax: x in a and
Ay: a in { V where V is finite Subset of X : card V <= 2 } by TARSKI:def 4;
consider V being finite Subset of X such that
A2: ( a = V & card V <= 2 ) by Ay;
thus x in X by Ax, A2; :: thesis: verum

end;

thus X c= union { V where V is finite Subset of X : card V <= 2 } :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in union { V where V is finite Subset of X : card V <= 2 } )
A2a: card {x} = 1 by CARD_1:30;
B2: x in {x} by TARSKI:def 1;
assume x in X ; :: thesis: x in union { V where V is finite Subset of X : card V <= 2 }
then {x} c= X by ZFMISC_1:31;
then {x} in { V where V is finite Subset of X : card V <= 2 } by A2a;
hence x in union { V where V is finite Subset of X : card V <= 2 } by B2, TARSKI:def 4; :: thesis: verum

end;