let G1, G2 be Universe; :: thesis: for a being Element of G1 st not a in G2 holds
G2 in G1
let a be Element of G1; :: thesis: ( not a in G2 implies G2 in G1 )
assume A1: not a in G2 ; :: thesis: G2 in G1
A2: G1 is Grothendieck of {a} by CLASSES3:def 4;

A3: now :: thesis: not {a} meets G2

assume {a} meets G2 ; :: thesis: contradiction
then not {a} /\ G2 is empty ;
then consider z being object such that
A4: z in {a} /\ G2 ;
( z in {a} & z in G2 ) by A4, XBOOLE_0:def 4;
hence contradiction by A1, TARSKI:def 1; :: thesis: verum

end;

now :: thesis: not G1 in G2

assume A5: G1 in G2 ; :: thesis: contradiction
( G2 is axiom_GU1 & G2 is axiom_GU3 ) ;
hence contradiction by A1, A5; :: thesis: verum

end;

hence G2 in G1 by A3, A2, Th78, CLASSES2:52; :: thesis: verum