environ
vocabularies ENUMSET;
notations ENUMSET;
constructors ENUMSET;
definitions ENUMSET;
equalities ENUMSET;
theorems ENUMSET;
begin
reserve a,x,y,z,A,B,C for set;
for A holds {} c= A
proof
let A;
thus {} c= A
proof
let x;
:: assume a: x in {};
:: thus x in A by a,ENUMSET:def 1;
assume x in {};
:: thus then x in A by ENUMSET:def 1;
hence x in A by ENUMSET:def 1;
end;
end;
for A holds A c= A
proof
let A;
thus A c= A
proof
let a;
assume a in A;
hence a in A;
end;
end;
for A,B,C holds A c= B & B c= C implies A c= C
proof
let A,B,C;
assume i: A c= B & B c= C;
thus A c= C
proof
let a;
assume a in A;
then a in B by i,ENUMSET:def 10;
hence a in C by i,ENUMSET:def 10;
end;
end;
A c= B & B c= C implies A c= C
proof
assume i: A c= B & B c= C;
thus A c= C
proof
let a;
assume a in A;
then a in B by i,ENUMSET:def 10;
hence a in C by i,ENUMSET:def 10;
end;
end;