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