let A1, A2 be set ; :: thesis: ( ( for x being object holds

( x in A1 iff ex S being non empty non void strict ManySortedSign st

( x = S & the carrier of S c= A & the carrier' of S c= A ) ) ) & ( for x being object holds

( x in A2 iff ex S being non empty non void strict ManySortedSign st

( x = S & the carrier of S c= A & the carrier' of S c= A ) ) ) implies A1 = A2 )

assume that

A17: for x being object holds

( x in A1 iff ex S being non empty non void strict ManySortedSign st

( x = S & the carrier of S c= A & the carrier' of S c= A ) ) and

A18: for x being object holds

( x in A2 iff ex S being non empty non void strict ManySortedSign st

( x = S & the carrier of S c= A & the carrier' of S c= A ) ) ; :: thesis: A1 = A2

thus A1 c= A2 :: according to XBOOLE_0:def 10 :: thesis: A2 c= A1

( x in A1 iff ex S being non empty non void strict ManySortedSign st

( x = S & the carrier of S c= A & the carrier' of S c= A ) ) ) & ( for x being object holds

( x in A2 iff ex S being non empty non void strict ManySortedSign st

( x = S & the carrier of S c= A & the carrier' of S c= A ) ) ) implies A1 = A2 )

assume that

A17: for x being object holds

( x in A1 iff ex S being non empty non void strict ManySortedSign st

( x = S & the carrier of S c= A & the carrier' of S c= A ) ) and

A18: for x being object holds

( x in A2 iff ex S being non empty non void strict ManySortedSign st

( x = S & the carrier of S c= A & the carrier' of S c= A ) ) ; :: thesis: A1 = A2

thus A1 c= A2 :: according to XBOOLE_0:def 10 :: thesis: A2 c= A1

proof

thus
A2 c= A1
:: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A1 or x in A2 )

assume x in A1 ; :: thesis: x in A2

then ex S being non empty non void strict ManySortedSign st

( x = S & the carrier of S c= A & the carrier' of S c= A ) by A17;

hence x in A2 by A18; :: thesis: verum

end;assume x in A1 ; :: thesis: x in A2

then ex S being non empty non void strict ManySortedSign st

( x = S & the carrier of S c= A & the carrier' of S c= A ) by A17;

hence x in A2 by A18; :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A2 or x in A1 )

assume x in A2 ; :: thesis: x in A1

then ex S being non empty non void strict ManySortedSign st

( x = S & the carrier of S c= A & the carrier' of S c= A ) by A18;

hence x in A1 by A17; :: thesis: verum

end;assume x in A2 ; :: thesis: x in A1

then ex S being non empty non void strict ManySortedSign st

( x = S & the carrier of S c= A & the carrier' of S c= A ) by A18;

hence x in A1 by A17; :: thesis: verum