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

proof

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

per cases ( s = f or s = g ) by A1, TARSKI:def 2;

suppose s = f ; :: thesis: a in {the carrier of f,the carrier of g}

hence a in {the carrier of f,the carrier of g} by A1, TARSKI:def 2; :: thesis: verum

end;

suppose s = g ; :: thesis: a in {the carrier of f,the carrier of g}

hence a in {the carrier of f,the carrier of g} by A1, TARSKI:def 2; :: thesis: verum

end;

end;

end;

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

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in {the carrier of f,the carrier of g} or a in Carr {f,g} )
assume A2: a in {the carrier of f,the carrier of g} ; :: thesis: a in Carr {f,g}
A3: ( f in {f,g} & g in {f,g} ) by TARSKI:def 2;

per cases ( a = the carrier of f or a = the carrier of g ) by A2, TARSKI:def 2;

suppose a = the carrier of f ; :: thesis: a in Carr {f,g}

hence a in Carr {f,g} by A3, Def7; :: thesis: verum

end;

suppose a = the carrier of g ; :: thesis: a in Carr {f,g}

hence a in Carr {f,g} by A3, Def7; :: thesis: verum

end;

end;

end;