let f be 1-sorted ; :: thesis: Carr {f} = { the carrier of f}
thus Carr {f} c= { the carrier of f} :: according to XBOOLE_0:def 10 :: thesis: { the carrier of f} c= Carr {f}

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Carr {f} or a in { the carrier of f} )
assume a in Carr {f} ; :: thesis: a in { the carrier of f}
then consider s being 1-sorted such that
A1: s in {f} and
A2: a = the carrier of s by Def7;
s = f by A1, TARSKI:def 1;
hence a in { the carrier of f} by A2, TARSKI:def 1; :: thesis: verum

end;

A3: f in {f} by TARSKI:def 1;
thus { the carrier of f} c= Carr {f} :: thesis: verum

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { the carrier of f} or a in Carr {f} )
assume a in { the carrier of f} ; :: thesis: a in Carr {f}
then a = the carrier of f by TARSKI:def 1;
hence a in Carr {f} by A3, Def7; :: thesis: verum

end;