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

( 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

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: verumhereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: the carrier of S2 c= the carrier of S1

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of S2 or x in 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;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

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