consider G0 being Element of V;
set M = Morphs G0,G0;
set S = { (Morphs G,H) where G, H is Element of V : G <= H } ;
( ID G0 is Element of Morphs G0,G0 & Morphs G0,G0 in { (Morphs G,H) where G, H is Element of V : G <= H } ) by Def15;
then reconsider T = union { (Morphs G,H) where G, H is Element of V : G <= H } as non empty set by TARSKI:def 4;
A1: for x being set holds
( x in T iff ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) )

proof

let x be set ; :: thesis: ( x in T iff ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) )
thus ( x in T implies ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) ) :: thesis: ( ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) implies x in T )

proof

assume x in T ; :: thesis: ex G, H being Element of V st
( G <= H & x is Morphism of G,H )
then consider Y being set such that
A2: x in Y and
A3: Y in { (Morphs G,H) where G, H is Element of V : G <= H } by TARSKI:def 4;
consider G, H being Element of V such that
A4: Y = Morphs G,H and
A5: G <= H by A3;
take G ; :: thesis: ex H being Element of V st
( G <= H & x is Morphism of G,H )
take H ; :: thesis: ( G <= H & x is Morphism of G,H )
x is Element of Morphs G,H by A2, A4;
hence ( G <= H & x is Morphism of G,H ) by A5; :: thesis: verum

end;

thus ( ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) implies x in T ) :: thesis: verum

proof

given G, H being Element of V such that A6: ( G <= H & x is Morphism of G,H ) ; :: thesis: x in T
set M = Morphs G,H;
( x in Morphs G,H & Morphs G,H in { (Morphs G,H) where G, H is Element of V : G <= H } ) by A6, Def15;
hence x in T by TARSKI:def 4; :: thesis: verum

end;

end;

now

let x be set ; :: thesis: ( x in T implies x is strict RingMorphism )
assume x in T ; :: thesis: x is strict RingMorphism
then ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) by A1;
hence x is strict RingMorphism ; :: thesis: verum

end;

then reconsider T' = T as RingMorphism_DOMAIN by Def13;
take T' ; :: thesis: for x being set holds
( x in T' iff ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) )
thus for x being set holds
( x in T' iff ex G, H being Element of V st
( G <= H & x is Morphism of G,H ) ) by A1; :: thesis: verum