let I1, I2 be Function of (InclPoset (Aux L)),(MonSet L); :: thesis: ( ( for AR being auxiliary Relation of L holds I1 . AR = AR -below ) & ( for AR being auxiliary Relation of L holds I2 . AR = AR -below ) implies I1 = I2 )
assume A3: for AR being auxiliary Relation of L holds I1 . AR = AR -below ; :: thesis: ( ex AR being auxiliary Relation of L st not I2 . AR = AR -below or I1 = I2 )
assume A4: for AR being auxiliary Relation of L holds I2 . AR = AR -below ; :: thesis: I1 = I2
dom I1 = the carrier of (InclPoset (Aux L)) by FUNCT_2:def 1;
then A5: dom I1 = Aux L by YELLOW_1:1;
dom I2 = the carrier of (InclPoset (Aux L)) by FUNCT_2:def 1;
then A6: dom I2 = Aux L by YELLOW_1:1;

now :: thesis: for a being object st a in Aux L holds
I1 . a = I2 . a

let a be object ; :: thesis: ( a in Aux L implies I1 . a = I2 . a )
assume a in Aux L ; :: thesis: I1 . a = I2 . a
then reconsider AR = a as auxiliary Relation of L by Def8;
I1 . AR = AR -below by A3
.= I2 . AR by A4 ;
hence I1 . a = I2 . a ; :: thesis: verum

end;

hence I1 = I2 by A5, A6, FUNCT_1:2; :: thesis: verum