now :: thesis: for o being object st o in {a,b,c} holds
o in the carrier of L

let o be object ; :: thesis: ( o in {a,b,c} implies b₁ in the carrier of L )
assume o in {a,b,c} ; :: thesis: b₁ in the carrier of L

per cases then ( o = a or o = b or o = c ) by ENUMSET1:def 1;

suppose o = a ; :: thesis: b₁ in the carrier of L

hence o in the carrier of L ; :: thesis: verum

end;

suppose o = b ; :: thesis: b₁ in the carrier of L

hence o in the carrier of L ; :: thesis: verum

end;

suppose o = c ; :: thesis: b₁ in the carrier of L

hence o in the carrier of L ; :: thesis: verum

end;

end;

end;

then {a,b,c} c= the carrier of L ;
hence {a,b,c} is Subset of L ; :: thesis: verum