set X = { [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs F,G : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2 ) * (F . g) = (G . h) * (o1 `2 ) ) } ;
commaObjs F,G = { [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom (F . c),(G . d) } by A1, Def5;
then [[c1,d1],f1] in commaObjs F,G by A1;
then reconsider o = [[c1,d1],f1] as Element of commaObjs F,G ;
( dom f1 = F . c1 & cod f1 = G . d1 ) by A1, CAT_1:18;
then ( dom (id c1) = c1 & cod (id c1) = c1 & dom (id d1) = d1 & cod (id d1) = d1 & (o `1 ) `1 = o `11 & (o `1 ) `2 = o `12 & o `1 = [c1,d1] & [c1,d1] `1 = c1 & [c1,d1] `2 = d1 & o `2 = f1 & f1 * (id (F . c1)) = f1 & (id (G . d1)) * f1 = f1 & F . (id c1) = id (F . c1) & G . (id d1) = id (G . d1) ) by CAT_1:44, CAT_1:46, CAT_1:47, CAT_1:108, MCART_1:7, MCART_1:def 14, MCART_1:def 15;
then A2: [[o,o],[(id c1),(id d1)]] in { [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs F,G : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2 ) * (F . g) = (G . h) * (o1 `2 ) ) } ;
{ [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs F,G : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2 ) * (F . g) = (G . h) * (o1 `2 ) ) } c= [:[:(commaObjs F,G),(commaObjs F,G):],[:the carrier' of C,the carrier' of D:]:]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs F,G : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2 ) * (F . g) = (G . h) * (o1 `2 ) ) } or x in [:[:(commaObjs F,G),(commaObjs F,G):],[:the carrier' of C,the carrier' of D:]:] )
assume x in { [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs F,G : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2 ) * (F . g) = (G . h) * (o1 `2 ) ) } ; :: thesis: x in [:[:(commaObjs F,G),(commaObjs F,G):],[:the carrier' of C,the carrier' of D:]:]
then ex g being Morphism of C ex h being Morphism of D ex o1, o2 being Element of commaObjs F,G st
( x = [[o1,o2],[g,h]] & dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2 ) * (F . g) = (G . h) * (o1 `2 ) ) ;
hence x in [:[:(commaObjs F,G),(commaObjs F,G):],[:the carrier' of C,the carrier' of D:]:] ; :: thesis: verum

end;

hence { [[o1,o2],[g,h]] where g is Morphism of C, h is Morphism of D, o1, o2 is Element of commaObjs F,G : ( dom g = o1 `11 & cod g = o2 `11 & dom h = o1 `12 & cod h = o2 `12 & (o2 `2 ) * (F . g) = (G . h) * (o1 `2 ) ) } is non empty Subset of [:[:(commaObjs F,G),(commaObjs F,G):],[:the carrier' of C,the carrier' of D:]:] by A2; :: thesis: verum