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

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

hence
{A,B,C} is Subset-Family of X
; :: thesis: verum
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;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