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

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

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