:: SUBSET semantic presentation

theorem Th1: :: SUBSET:1

for b₁, b₂ being set st b₁ in b₂ holds
b₁ is Element of b₂

proof end;

theorem Th2: :: SUBSET:2

for b₁, b₂ being set st b₁ is Element of b₂ & not b₂ is empty holds
b₁ in b₂ by SUBSET_1:def 2;

theorem Th3: :: SUBSET:3

for b₁, b₂ being set holds
( b₁ is Subset of b₂ iff b₁ c= b₂ )

proof end;

theorem Th4: :: SUBSET:4

for b₁, b₂, b₃ being set st b₁ in b₂ & b₂ is Subset of b₃ holds
b₁ is Element of b₃

proof end;

theorem Th5: :: SUBSET:5

for b₁, b₂, b₃ being set st b₁ in b₂ & b₂ is Subset of b₃ holds
not b₃ is empty

proof end;