let S1, S2 be non empty strict full SubRelStr of MonMaps (L,L); :: thesis: ( ( for f being Function of L,L holds
( f is Element of S1 iff f is closure ) ) & ( for f being Function of L,L holds
( f is Element of S2 iff f is closure ) ) implies S1 = S2 )
assume that
A6: for f being Function of L,L holds
( f is Element of S1 iff f is closure ) and
A7: for f being Function of L,L holds
( f is Element of S2 iff f is closure ) ; :: thesis: S1 = S2
the carrier of S1 = the carrier of S2

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: the carrier of S2 c= the carrier of S1

let x be object ; :: thesis: ( x in the carrier of S1 implies x in the carrier of S2 )
assume x in the carrier of S1 ; :: thesis: x in the carrier of S2
then reconsider y = x as Element of S1 ;
y is Element of (MonMaps (L,L)) by YELLOW_0:58;
then reconsider y = y as Function of L,L by Th9;
y is closure by A6;
then y is Element of S2 by A7;
hence x in the carrier of S2 ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of S2 or x in the carrier of S1 )
assume x in the carrier of S2 ; :: thesis: x in the carrier of S1
then reconsider y = x as Element of S2 ;
y is Element of (MonMaps (L,L)) by YELLOW_0:58;
then reconsider y = y as Function of L,L by Th9;
y is closure by A7;
then y is Element of S1 by A6;
hence x in the carrier of S1 ; :: thesis: verum

end;

hence S1 = S2 by YELLOW_0:57; :: thesis: verum