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 object ; :: 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
A1: x in a and
A2: 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
A3: ( a = V & card V <= 2 ) by A2;
thus x in X by A1, A3; :: thesis: verum
end;
thus X c= union { V where V is finite Subset of X : card V <= 2 } :: thesis: verum
proof
let x be object ; :: 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 } )
A4: card {x} = 1 by CARD_1:30;
A5: 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 A4;
hence x in union { V where V is finite Subset of X : card V <= 2 } by A5, TARSKI:def 4; :: thesis: verum
end;