consider x being Element of Q. I such that
A2: u = QClass. x by Def5;
x `1 <> 0. I

proof

assume x `1 = 0. I ; :: thesis: contradiction
then A3: x in q0. I by Def8;
x in u by A2, Th6;
then u meets q0. I by A3, XBOOLE_0:3;
hence contradiction by A1, Th9; :: thesis: verum

end;

then reconsider t = [(x `2 ),(x `1 )] as Element of Q. I by Def1;
set M = QClass. t;
A4: for z being Element of Q. I st ex a being Element of Q. I st
( a in u & (z `1 ) * (a `1 ) = (z `2 ) * (a `2 ) ) holds
z in QClass. t

proof

let z be Element of Q. I; :: thesis: ( ex a being Element of Q. I st
( a in u & (z `1 ) * (a `1 ) = (z `2 ) * (a `2 ) ) implies z in QClass. t )
given a being Element of Q. I such that A5: a in u and
A6: (z `1 ) * (a `1 ) = (z `2 ) * (a `2 ) ; :: thesis: z in QClass. t
A7: (a `1 ) * (x `2 ) = (a `2 ) * (x `1 ) by A2, A5, Def4;
A8: ((z `1 ) * (t `2 )) * (a `2 ) = ((z `1 ) * (x `1 )) * (a `2 ) by MCART_1:def 2
.= (z `1 ) * ((a `1 ) * (x `2 )) by A7, GROUP_1:def 4
.= ((z `2 ) * (a `2 )) * (x `2 ) by A6, GROUP_1:def 4
.= ((z `2 ) * (a `2 )) * (t `1 ) by MCART_1:def 1
.= ((z `2 ) * (t `1 )) * (a `2 ) by GROUP_1:def 4 ;
A9: a `2 <> 0. I by Th2;
a `2 divides a `2 ;
then A10: a `2 divides ((z `2 ) * (t `1 )) * (a `2 ) by GCD_1:7;
a `2 divides a `2 ;
then A11: a `2 divides ((z `1 ) * (t `2 )) * (a `2 ) by GCD_1:7;
(z `1 ) * (t `2 ) = ((z `1 ) * (t `2 )) * (1_ I) by VECTSP_1:def 13
.= ((z `1 ) * (t `2 )) * ((a `2 ) / (a `2 )) by A9, GCD_1:9
.= (((z `2 ) * (t `1 )) * (a `2 )) / (a `2 ) by A9, A8, A11, GCD_1:11
.= ((z `2 ) * (t `1 )) * ((a `2 ) / (a `2 )) by A9, A10, GCD_1:11
.= ((z `2 ) * (t `1 )) * (1_ I) by A9, GCD_1:9
.= (z `2 ) * (t `1 ) by VECTSP_1:def 13 ;
hence z in QClass. t by Def4; :: thesis: verum

end;

for z being Element of Q. I st z in QClass. t holds
ex a being Element of Q. I st
( a in u & (z `1 ) * (a `1 ) = (z `2 ) * (a `2 ) )

proof

let z be Element of Q. I; :: thesis: ( z in QClass. t implies ex a being Element of Q. I st
( a in u & (z `1 ) * (a `1 ) = (z `2 ) * (a `2 ) ) )
assume z in QClass. t ; :: thesis: ex a being Element of Q. I st
( a in u & (z `1 ) * (a `1 ) = (z `2 ) * (a `2 ) )
then (z `1 ) * (t `2 ) = (z `2 ) * (t `1 ) by Def4;
then (z `1 ) * (x `1 ) = (z `2 ) * (t `1 ) by MCART_1:def 2
.= (z `2 ) * (x `2 ) by MCART_1:def 1 ;
hence ex a being Element of Q. I st
( a in u & (z `1 ) * (a `1 ) = (z `2 ) * (a `2 ) ) by A2, Th6; :: thesis: verum

end;

hence ex b₁ being Element of Quot. I st
for z being Element of Q. I holds
( z in b₁ iff ex a being Element of Q. I st
( a in u & (z `1 ) * (a `1 ) = (z `2 ) * (a `2 ) ) ) by A4; :: thesis: verum