:: SUBSET  semantic presentation begin  
theorem :: SUBSET:1 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "b")))) "holds"  (Bool (Set (Var "a")) "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "b")))) ; 
 
theorem :: SUBSET:2 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a")) "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "b"))) & (Bool (Bool  "not" (Set (Var "b")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "holds"  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "b")))) ; 
 
theorem :: SUBSET:3 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "a")) "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "b"))) "iff" (Bool (Set (Var "a"))  ($#r1_tarski :::"c="::: )  (Set (Var "b")))  ")" )) ; 
 
theorem :: SUBSET:4 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "b"))) & (Bool (Set (Var "b")) "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "c")))) "holds"  (Bool (Set (Var "a")) "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "c")))) ; 
 
theorem :: SUBSET:5 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "b"))) & (Bool (Set (Var "b")) "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "c")))) "holds"  (Bool  "not" (Bool (Set (Var "c")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) ;