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 ;
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 ; :: 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 ; :: 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 ;
suppose a = the carrier of f ; :: thesis: a in Carr {f,g}
hence a in Carr {f,g} by ; :: thesis: verum
end;
suppose a = the carrier of g ; :: thesis: a in Carr {f,g}
hence a in Carr {f,g} by ; :: thesis: verum
end;
end;
end;