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}

thus { the carrier of f} c= Carr {f} :: thesis: verum

thus Carr {f} c= { the carrier of f} :: according to XBOOLE_0:def 10 :: thesis: { the carrier of f} c= Carr {f}

proof

A3:
f in {f}
by TARSKI:def 1;
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;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

thus { the carrier of f} c= Carr {f} :: thesis: verum