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 object ; :: 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} and
A2: 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 A2, 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 A2, 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 object ; :: according to TARSKI:def 3 :: thesis: ( not a in { the carrier of f, the carrier of g} or a in Carr {f,g} )
A3: f in {f,g} by TARSKI:def 2;
A4: g in {f,g} by TARSKI:def 2;
assume A5: a in { the carrier of f, the carrier of g} ; :: thesis: a in Carr {f,g}

per cases ( a = the carrier of f or a = the carrier of g ) by A5, 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 A4, Def7; :: thesis: verum

end;

end;

end;