let X be set ; :: thesis: for A, B, C being Subset of X holds {A,B,C} is Subset-Family of X
let A, B, C be Subset of X; :: thesis: {A,B,C} is Subset-Family of X
set D = {A,B,C};
{A,B,C} c= bool X
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {A,B,C} or x in bool X )
assume x in {A,B,C} ; :: thesis: x in bool X
then ( x = A or x = B or x = C ) by ENUMSET1:def 1;
hence x in bool X ; :: thesis: verum
end;
hence {A,B,C} is Subset-Family of X ; :: thesis: verum